---

Step * of Lemma approx-per-trans

∀[T:Type]. Trans(Base;x,y.approx-per(T;x;y))
BY
{ (Auto THEN D 0 THEN Auto THEN D -2 THEN D -1 THEN D 0 THEN ExRepD THEN (Complete (Auto) ORELSE D 0)) }

1
1. [T] : Type
2. a : Base
3. b : Base
4. c : Base
5. t3 : Base
6. a ≤ t3
7. t3 ∈ T
8. t2 : Base
9. b ≤ t2
10. t2 ∈ T
11. ∀t:Base. (((a ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((b ≤ t') ∧ (t' = t ∈ T))))
12. ∀t:Base. (((b ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((a ≤ t') ∧ (t' = t ∈ T))))
13. t1 : Base
14. b ≤ t1
15. t1 ∈ T
16. t : Base
17. c ≤ t
18. t ∈ T
19. ∀t:Base. (((b ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((c ≤ t') ∧ (t' = t ∈ T))))
20. ∀t:Base. (((c ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((b ≤ t') ∧ (t' = t ∈ T))))
⊢ ∀t:Base. (((a ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((c ≤ t') ∧ (t' = t ∈ T))))

2
1. [T] : Type
2. a : Base
3. b : Base
4. c : Base
5. t3 : Base
6. a ≤ t3
7. t3 ∈ T
8. t2 : Base
9. b ≤ t2
10. t2 ∈ T
11. ∀t:Base. (((a ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((b ≤ t') ∧ (t' = t ∈ T))))
12. ∀t:Base. (((b ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((a ≤ t') ∧ (t' = t ∈ T))))
13. t1 : Base
14. b ≤ t1
15. t1 ∈ T
16. t : Base
17. c ≤ t
18. t ∈ T
19. ∀t:Base. (((b ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((c ≤ t') ∧ (t' = t ∈ T))))
20. ∀t:Base. (((c ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((b ≤ t') ∧ (t' = t ∈ T))))
⊢ ∀t:Base. (((c ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((a ≤ t') ∧ (t' = t ∈ T))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  Trans(Base;x,y.approx-per(T;x;y))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  -2  THEN  D  -1  THEN  D  0  THEN  ExRepD  THEN  (Complete  (Auto)  ORELSE  D  0))

---

Home Index