---

Step * 1 1 of Lemma ex-approx_transitivity


1. e : Atom2
2. t1 : Base
3. t2 : Base
4. t3 : Base
5. ∀f:Base. (e#f:Base ⇒ (f t2?e:v.⊥ ≤ f t3?e:v.⊥))
6. ∀f:Base. (e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t2?e:v.⊥))
7. f : Base
8. e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t2?e:v.⊥)
⊢ e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t3?e:v.⊥)
BY
{ (((D 5 With ⌜f⌝  THENA Auto) THEN (At ⌜Type⌝ (D 0)⋅ THENA Auto)) THEN ThinTrivial) }

1
1. e : Atom2
2. t1 : Base
3. t2 : Base
4. t3 : Base
5. ∀f:Base. (e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t2?e:v.⊥))
6. f : Base
7. e#f:Base
8. f t2?e:v.⊥ ≤ f t3?e:v.⊥
9. f t1?e:v.⊥ ≤ f t2?e:v.⊥
⊢ f t1?e:v.⊥ ≤ f t3?e:v.⊥

---

Latex:

---

Latex:

1.  e  :  Atom2
2.  t1  :  Base
3.  t2  :  Base
4.  t3  :  Base
5.  \mforall{}f:Base.  (e\#f:Base  {}\mRightarrow{}  (f  t2?e:v.\mbot{}  \mleq{}  f  t3?e:v.\mbot{}))
6.  \mforall{}f:Base.  (e\#f:Base  {}\mRightarrow{}  (f  t1?e:v.\mbot{}  \mleq{}  f  t2?e:v.\mbot{}))
7.  f  :  Base
8.  e\#f:Base  {}\mRightarrow{}  (f  t1?e:v.\mbot{}  \mleq{}  f  t2?e:v.\mbot{})
\mvdash{}  e\#f:Base  {}\mRightarrow{}  (f  t1?e:v.\mbot{}  \mleq{}  f  t3?e:v.\mbot{})


By

---

Latex:
(((D  5  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))  THEN  ThinTrivial)

---

Home Index