---

Step * 1 of Lemma decidable__cmp-le

.....equality..... 
1. T : Type
2. cmp : comparison(T)@i
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ ((cmp x y) = 0 ∈ ℤ)))
6. x ∈ T
7. x1 ∈ T
8. (cmp x x1) = 0 ∈ ℤ
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ ((cmp x y) = 0 ∈ ℤ)))
12. y ∈ T
13. y1 ∈ T
14. (cmp y y1) = 0 ∈ ℤ
⊢ cmp x1 y1 ~ cmp x y
BY
{ (D 2 THEN Auto) }

1
1. T : Type
2. cmp : T ⟶ T ⟶ ℤ@i
3. ∀x,y:T.  ((cmp x y) = (-(cmp y x)) ∈ ℤ)
4. ∀x,y:T.  (((cmp x y) = 0 ∈ ℤ) ⇒ (∀z:T. ((cmp x z) = (cmp y z) ∈ ℤ)))
5. ∀x,y,z:T.  ((0 ≤ (cmp x y)) ⇒ (0 ≤ (cmp y z)) ⇒ (0 ≤ (cmp x z)))
6. x : Base
7. x1 : Base
8. x = x1 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ ((cmp x y) = 0 ∈ ℤ)))
9. x ∈ T
10. x1 ∈ T
11. (cmp x x1) = 0 ∈ ℤ
12. y : Base
13. y1 : Base
14. y = y1 ∈ pertype(λx,y. ((x ∈ T) ∧ (y ∈ T) ∧ ((cmp x y) = 0 ∈ ℤ)))
15. y ∈ T
16. y1 ∈ T
17. (cmp y y1) = 0 ∈ ℤ
⊢ (cmp x1 y1) = (cmp x y) ∈ ℤ

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  cmp  :  comparison(T)@i
3.  x  :  Base
4.  x1  :  Base
5.  x  =  x1
6.  x  \mmember{}  T
7.  x1  \mmember{}  T
8.  (cmp  x  x1)  =  0
9.  y  :  Base
10.  y1  :  Base
11.  y  =  y1
12.  y  \mmember{}  T
13.  y1  \mmember{}  T
14.  (cmp  y  y1)  =  0
\mvdash{}  cmp  x1  y1  \msim{}  cmp  x  y


By

---

Latex:
(D  2  THEN  Auto)

---

Home Index