---

Step * of Lemma cmp-le_wf

∀[T:Type]. ∀[cmp:comparison(T)]. ∀[x,y:cmp-type(T;cmp)].  (cmp-le(cmp;x;y) ∈ ℙ)
BY
{ ((Auto THEN OnVar `x' quotD THEN OnVar `y' quotD)
   THEN (RepUR ``cmp-le`` 0
         THEN D 2
         THEN Auto
         THEN (InstHyp [⌜x⌝;⌜x1⌝] 4⋅ THENA Auto)
         THEN (RWO "-1" 0 THENA Auto)
         THEN (RWO "3" 0 THENA Auto)
         THEN (InstHyp [⌜y⌝;⌜y1⌝] 4⋅ THENA Auto)
         THEN RWO "-1" 0
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[cmp:comparison(T)].  \mforall{}[x,y:cmp-type(T;cmp)].    (cmp-le(cmp;x;y)  \mmember{}  \mBbbP{})


By

---

Latex:
((Auto  THEN  OnVar  `x'  quotD  THEN  OnVar  `y'  quotD)
  THEN  (RepUR  ``cmp-le``  0
              THEN  D  2
              THEN  Auto
              THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
              THEN  (RWO  "-1"  0  THENA  Auto)
              THEN  (RWO  "3"  0  THENA  Auto)
              THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
              THEN  RWO  "-1"  0
              THEN  Auto)\mcdot{}
  )

---

Home Index