Step
*
1
of Lemma
not-id-sqle-bottom
1. λx.x ≤ ⊥
⊢ False
BY
{ TACTIC:((Assert λx.x ~ ⊥ BY
(Refine_sqequalSqle THEN Auto))
THEN (Assert ⌜(λx.x) 0 ~ (λx.x) 1⌝ BY
(HypSubst (-1) 0 THEN Strictness THEN Auto))
THEN (Assert 0 = 1 ∈ ℤ BY
(Reduce (-1) THEN HypSubst' -1 0 THEN Auto))
THEN Auto) }
Latex:
Latex:
1. \mlambda{}x.x \mleq{} \mbot{}
\mvdash{} False
By
Latex:
TACTIC:((Assert \mlambda{}x.x \msim{} \mbot{} BY
(Refine\_sqequalSqle THEN Auto))
THEN (Assert \mkleeneopen{}(\mlambda{}x.x) 0 \msim{} (\mlambda{}x.x) 1\mkleeneclose{} BY
(HypSubst (-1) 0 THEN Strictness THEN Auto))
THEN (Assert 0 = 1 BY
(Reduce (-1) THEN HypSubst' -1 0 THEN Auto))
THEN Auto)
Home
Index