---

Step * 3 1 of Lemma comparison-linear

.....assertion..... 
1. T : Type
2. cmp : comparison(T)
3. x : cmp-type(T;cmp)
4. y : cmp-type(T;cmp)
5. ¬cmp-le(cmp;x;y)
6. ¬cmp-le(cmp;y;x)
⊢ 0 = 1 ∈ ℤ
BY
{ ((OnVar `x' newQuotD THEN Try ((RWO "comparison-reflexive" 0 THEN Auto))⋅)
   THEN OnVar `y' newQuotD
   THEN (Try ((RWO "comparison-reflexive" 0 THEN Auto))
         THEN (D 2 THEN Auto)
         THEN All (RepUR ``cmp-le``)
         THEN RWO "3" (-1)
         THEN Auto')⋅) }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  cmp  :  comparison(T)
3.  x  :  cmp-type(T;cmp)
4.  y  :  cmp-type(T;cmp)
5.  \mneg{}cmp-le(cmp;x;y)
6.  \mneg{}cmp-le(cmp;y;x)
\mvdash{}  0  =  1


By

---

Latex:
((OnVar  `x'  newQuotD  THEN  Try  ((RWO  "comparison-reflexive"  0  THEN  Auto))\mcdot{})
  THEN  OnVar  `y'  newQuotD
  THEN  (Try  ((RWO  "comparison-reflexive"  0  THEN  Auto))
              THEN  (D  2  THEN  Auto)
              THEN  All  (RepUR  ``cmp-le``)
              THEN  RWO  "3"  (-1)
              THEN  Auto')\mcdot{})

---

Home Index