---

Step * 2 1 1 1 of Lemma comparison-linear


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 ∈ ℤ
BY
{ (D 2 THEN Auto THEN FHyp 5 [-2;-3] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  istype(T)
4.  \mforall{}x,y:T.    istype((cmp  x  y)  =  0)
5.  \mforall{}x:T.  ((cmp  x  x)  =  0)
6.  a1  :  Base
7.  a1  \mmember{}  T
8.  istype(T)
9.  \mforall{}x,y:T.    istype((cmp  x  y)  =  0)
10.  \mforall{}x:T.  ((cmp  x  x)  =  0)
11.  a  :  Base
12.  a  \mmember{}  T
13.  istype(T)
14.  \mforall{}x,y:T.    istype((cmp  x  y)  =  0)
15.  \mforall{}x:T.  ((cmp  x  x)  =  0)
16.  a2  :  Base
17.  a2  \mmember{}  T
18.  0  \mleq{}  (cmp  a1  a)
19.  0  \mleq{}  (cmp  a  a2)
20.  \mneg{}(0  \mleq{}  (cmp  a1  a2))
\mvdash{}  0  =  1


By

---

Latex:
(D  2  THEN  Auto  THEN  FHyp  5  [-2;-3]  THEN  Auto)

---

Home Index