Step
*
1
1
of Lemma
decidable__cmp-le
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) ∈ ℤ
BY
{ ((Assert ∀z:T. ((cmp x z) = (cmp x1 z) ∈ ℤ) BY Auto) THEN (Assert ∀z:T. ((cmp y z) = (cmp y1 z) ∈ ℤ) BY 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 ∈ ℤ
18. ∀z:T. ((cmp x z) = (cmp x1 z) ∈ ℤ)
19. ∀z:T. ((cmp y z) = (cmp y1 z) ∈ ℤ)
⊢ (cmp x1 y1) = (cmp x y) ∈ ℤ
Latex:
Latex:
1. T : Type
2. cmp : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbZ{}@i
3. \mforall{}x,y:T. ((cmp x y) = (-(cmp y x)))
4. \mforall{}x,y:T. (((cmp x y) = 0) {}\mRightarrow{} (\mforall{}z:T. ((cmp x z) = (cmp y z))))
5. \mforall{}x,y,z:T. ((0 \mleq{} (cmp x y)) {}\mRightarrow{} (0 \mleq{} (cmp y z)) {}\mRightarrow{} (0 \mleq{} (cmp x z)))
6. x : Base
7. x1 : Base
8. x = x1
9. x \mmember{} T
10. x1 \mmember{} T
11. (cmp x x1) = 0
12. y : Base
13. y1 : Base
14. y = y1
15. y \mmember{} T
16. y1 \mmember{} T
17. (cmp y y1) = 0
\mvdash{} (cmp x1 y1) = (cmp x y)
By
Latex:
((Assert \mforall{}z:T. ((cmp x z) = (cmp x1 z)) BY
Auto)
THEN (Assert \mforall{}z:T. ((cmp y z) = (cmp y1 z)) BY
Auto)
)
Home
Index