Step
*
1
1
of Lemma
dM-0-not-1
1. I : fset(ℕ)
⊢ ¬(0 = 1 ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))
BY
{ ((Subst' 0 ~ 0 0 THENA (RW (SubC (SymbCompC [] 100)) 0 THEN Auto))
   THEN (Subst' 1 ~ 1 0 THENA (RW (SubC (SymbCompC [] 100)) 0 THEN Auto))
   ) }
1
1. I : fset(ℕ)
⊢ ¬(0 = 1 ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))
Latex:
Latex:
1.  I  :  fset(\mBbbN{})
\mvdash{}  \mneg{}(0  =  1)
By
Latex:
((Subst'  0  \msim{}  0  0  THENA  (RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto))
  THEN  (Subst'  1  \msim{}  1  0  THENA  (RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto))
  )
Home
Index