---

Step * 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' before y ∈ before(e) @ [e] ⇐⇒ (e' <loc y) ∧ y ≤loc e 
BY
{ ((RWO "l_before_append_iff" 0 THENA Auto)
   THEN (RWO "l_before-es-before-iff" 0 THENA Auto)
   THEN (RWO "member-es-before" 0 THENA Auto)
   THEN (RWO "member_singleton" 0 THENA Auto)⋅) }

1
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 

---

Latex:



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


By

((RWO  "l\_before\_append\_iff"  0  THENA  Auto)
  THEN  (RWO  "l\_before-es-before-iff"  0  THENA  Auto)
  THEN  (RWO  "member-es-before"  0  THENA  Auto)
  THEN  (RWO  "member\_singleton"  0  THENA  Auto)\mcdot{})

---

Home Index