---

Step * of Lemma bool-cmp-zero

∀[x,y:𝔹].  uiff((bool-cmp() x y) = 0 ∈ ℤ;x = y)
BY
{ (RepeatFor 2 (((D 0 THENA Auto) THEN BoolInd (-1))) THEN RepUR ``bool-cmp`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbB{}].    uiff((bool-cmp()  x  y)  =  0;x  =  y)


By

---

Latex:
(RepeatFor  2  (((D  0  THENA  Auto)  THEN  BoolInd  (-1)))  THEN  RepUR  ``bool-cmp``  0  THEN  Auto)

---

Home Index