---

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

∀the_es:EO. ∀e,e',y:E.  (e' before y ∈ ≤loc(e) ⇐⇒ (e' <loc y) ∧ y ≤loc e )
BY
{ ((UnivCD THENA Auto) THEN Unfold `es-le-before` 0) }

1
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 

---

Latex:


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


By

((UnivCD  THENA  Auto)  THEN  Unfold  `es-le-before`  0)

---

Home Index