Library Scott
Scott's Theorem
Theorem
Scott
(
M
:
term
→
Prop
) :
M
<=1
closed
→
(
∀
s
t
,
M
s
→
closed
t
→
t
==
s
→
M
t
) →
(
∃
t1
,
closed
t1
∧
M
t1
) → (
∃
t2
,
closed
t2
∧
¬
M
t2
) →
¬
ldec
M
.
Applications of Scott's Theorem
Goal
¬
ldec
(
fun
x
⇒
closed
x
∧
converges
x
).
Lemma
I_neq_Omega
:
¬
I
==
Omega
.
Lemma
C27
:
∀
t
,
closed
t
→
¬
ldec
(
fun
x
⇒
closed
x
∧
x
==
t
).
Lemma
C27_proc
:
∀
t
,
proc
t
→
¬
ldec
(
fun
x
⇒
x
==
t
).
Lemma
Eq_ldec
:
¬
ldec
(
fun
x
⇒
∃
(
s
t
:
term
),
x
=
tenc
(
s
t
)
∧
s
==
t
).