---

Step * 2 1 1 of Lemma comparison-linear

.....assertion..... 
1. T : Type
2. cmp : comparison(T)
3. a : cmp-type(T;cmp)
4. b : cmp-type(T;cmp)
5. c : cmp-type(T;cmp)
6. cmp-le(cmp;a;b)
7. cmp-le(cmp;b;c)
8. ¬cmp-le(cmp;a;c)
⊢ 0 = 1 ∈ ℤ
BY
{ ((OnVar `a' newQuotD THEN Try ((RWO "comparison-reflexive" 0 THEN Auto))⋅)
   THEN OnVar `b' newQuotD
   THEN (Try ((RWO "comparison-reflexive" 0 THEN Auto))
         THEN OnVar `c' newQuotD
         THEN (Try ((RWO "comparison-reflexive" 0 THEN Auto))
               THEN ThinVar `b'⋅
               THEN ThinVar `b1'⋅
               THEN ThinVar `b2'⋅
               THEN All (RepUR ``cmp-le``))⋅)⋅)⋅ }

1
1. T : Type
2. cmp : comparison(T)
3. istype(T)
4. ∀x,y:T.  istype((cmp x y) = 0 ∈ ℤ)
5. ∀x:T. ((cmp x x) = 0 ∈ ℤ)
6. a1 : Base
7. a1 ∈ T
8. istype(T)
9. ∀x,y:T.  istype((cmp x y) = 0 ∈ ℤ)
10. ∀x:T. ((cmp x x) = 0 ∈ ℤ)
11. a : Base
12. a ∈ T
13. istype(T)
14. ∀x,y:T.  istype((cmp x y) = 0 ∈ ℤ)
15. ∀x:T. ((cmp x x) = 0 ∈ ℤ)
16. a2 : Base
17. a2 ∈ T
18. 0 ≤ (cmp a1 a)
19. 0 ≤ (cmp a a2)
20. ¬(0 ≤ (cmp a1 a2))
⊢ 0 = 1 ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  cmp  :  comparison(T)
3.  a  :  cmp-type(T;cmp)
4.  b  :  cmp-type(T;cmp)
5.  c  :  cmp-type(T;cmp)
6.  cmp-le(cmp;a;b)
7.  cmp-le(cmp;b;c)
8.  \mneg{}cmp-le(cmp;a;c)
\mvdash{}  0  =  1


By

---

Latex:
((OnVar  `a'  newQuotD  THEN  Try  ((RWO  "comparison-reflexive"  0  THEN  Auto))\mcdot{})
  THEN  OnVar  `b'  newQuotD
  THEN  (Try  ((RWO  "comparison-reflexive"  0  THEN  Auto))
              THEN  OnVar  `c'  newQuotD
              THEN  (Try  ((RWO  "comparison-reflexive"  0  THEN  Auto))
                          THEN  ThinVar  `b'\mcdot{}
                          THEN  ThinVar  `b1'\mcdot{}
                          THEN  ThinVar  `b2'\mcdot{}
                          THEN  All  (RepUR  ``cmp-le``))\mcdot{})\mcdot{})\mcdot{}

---

Home Index