---

Step * of Lemma comparison-equiv

∀[T:Type]. ∀cmp:comparison(T). EquivRel(T;x,y.(cmp x y) = 0 ∈ ℤ)
BY
{ TACTIC:(Auto THEN RepeatFor 2 ((D 0 THEN Auto)) THEN D 2 THEN Auto) }

1
1. T : Type
2. cmp : T ⟶ T ⟶ ℤ
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. a : T
⊢ (cmp a a) = 0 ∈ ℤ

2
1. T : Type
2. cmp : T ⟶ T ⟶ ℤ
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. a : T
7. b : T
8. (cmp a b) = 0 ∈ ℤ
⊢ (cmp b a) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}cmp:comparison(T).  EquivRel(T;x,y.(cmp  x  y)  =  0)


By

---

Latex:
TACTIC:(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto))  THEN  D  2  THEN  Auto)

---

Home Index