---

Step * of Lemma not-btrue-sqeq-bfalse

¬(ff ~ tt)
BY
{ (RepUR ``btrue bfalse`` 0 THEN Repeat (RW (SweepUpC CanonicalDiffC) 0) THEN Auto) }

---

Latex:

---

Latex:
\mneg{}(ff  \msim{}  tt)


By

---

Latex:
(RepUR  ``btrue  bfalse``  0  THEN  Repeat  (RW  (SweepUpC  CanonicalDiffC)  0)  THEN  Auto)

---

Home Index