---

Step * of Lemma l_before-es-before-iff

∀the_es:EO. ∀e,e',y:E.  (e' before y ∈ before(e) ⇐⇒ (e' <loc y) ∧ (y <loc e))
BY
{ Auto }

1
1. the_es : EO@i'
2. e : E@i
3. e' : E@i
4. y : E@i
5. e' before y ∈ before(e)@i
⊢ (e' <loc y)

2
1. the_es : EO@i'
2. e : E@i
3. e' : E@i
4. y : E@i
5. e' before y ∈ before(e)@i
⊢ (y <loc e)

3
1. the_es : EO@i'
2. e : E@i
3. e' : E@i
4. y : E@i
5. (e' <loc y)@i
6. (y <loc e)@i
⊢ e' before y ∈ before(e)

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e,e',y:E.    (e'  before  y  \mmember{}  before(e)  \mLeftarrow{}{}\mRightarrow{}  (e'  <loc  y)  \mwedge{}  (y  <loc  e\000C))


By

Auto

---

Home Index