---

Step * of Lemma assert-lattice-bless

∀[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  uiff(↑lattice-bless(l;eq;a;b);a < b)
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``lattice-bless lattice-less`` 0
   THEN (BoolCase ⌜lattice-ble(l;eq;a;b)⌝⋅ THENA Auto)
   THEN BoolCase ⌜eq a b⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:LatticeStructure].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[a,b:Point(l)].
    uiff(\muparrow{}lattice-bless(l;eq;a;b);a  <  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``lattice-bless  lattice-less``  0
  THEN  (BoolCase  \mkleeneopen{}lattice-ble(l;eq;a;b)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  BoolCase  \mkleeneopen{}eq  a  b\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index