---

Step * 1 of Lemma es-before_wf2


∀the_es:EO. ∀e:E.  (before(e) ∈ {e':E| loc(e') = loc(e) ∈ Id}  List)
BY
{ (StrongLocLessInd THEN RecUnfold `es-before` 0 THEN SplitOnConclITE THEN Auto) }

1
1. the_es : EO@i'
2. e : E@i
3. ∀x:E. ((x <loc e) ⇒ (before(x) ∈ {e':E| loc(e') = loc(x) ∈ Id}  List))
4. ¬↑first(e)
⊢ before(pred(e)) ∈ {e':E| loc(e') = loc(e) ∈ Id}  List

---

Latex:



\mforall{}the$_{es}$:EO.  \mforall{}e:E.    (before(e)  \mmember{}  \{e':E|  loc(e')  =  loc(e)\}    List)


By

(StrongLocLessInd  THEN  RecUnfold  `es-before`  0  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index