---

Step * 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.⊥))
⊢ ∀f:Base. (e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t3?e:v.⊥))
BY
{ ParallelLast }

1
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.⊥)

---

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{}))
\mvdash{}  \mforall{}f:Base.  (e\#f:Base  {}\mRightarrow{}  (f  t1?e:v.\mbot{}  \mleq{}  f  t3?e:v.\mbot{}))


By

---

Latex:
ParallelLast

---

Home Index