Step
*
1
1
of Lemma
not-0-eq-1
1. 0 = 1 ∈ ℤ
2. 0 ~ 1
⊢ False
BY
{ (Assert if 0=1 then False else True BY
         (Reduce 0 THEN TrueCD)) }
1
1. 0 = 1 ∈ ℤ
2. 0 ~ 1
3. if 0=1 then False else True
⊢ False
Latex:
Latex:
1.  0  =  1
2.  0  \msim{}  1
\mvdash{}  False
By
Latex:
(Assert  if  0=1  then  False  else  True  BY
              (Reduce  0  THEN  TrueCD))
Home
Index