---

Step * 1 1 1 of Lemma l_before-es-le-before-iff


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' <loc y) ∧ (y <loc e)) ∨ e' before y ∈ [e] ∨ ((e' <loc e) ∧ (y = e ∈ E))
BY
{ (D (-1) THEN Auto) }

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  y  :  E@i
5.  (e'  <loc  y)@i
6.  y  \mleq{}loc  e  @i
\mvdash{}  ((e'  <loc  y)  \mwedge{}  (y  <loc  e))  \mvee{}  e'  before  y  \mmember{}  [e]  \mvee{}  ((e'  <loc  e)  \mwedge{}  (y  =  e))


By

(D  (-1)  THEN  Auto)

---

Home Index