---

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