---

Step * 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
⊢ ((e' <loc y) ∧ (y <loc e)) ∨ e' before y ∈ [e] ∨ ((e' <loc e) ∧ (y = e ∈ E)) ⇐⇒ (e' <loc y) ∧ y ≤loc e 
BY
{ (Auto THEN SplitOrHyps THEN Auto THEN Try ((RWO "singleton_before" (-1) THEN Auto))) }

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

---

Latex:



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


By

(Auto  THEN  SplitOrHyps  THEN  Auto  THEN  Try  ((RWO  "singleton\_before"  (-1)  THEN  Auto)))

---

Home Index