---

Step * 1 1 of Lemma es-before_wf2


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
BY
{ ((InstHyp [pred(e)] 3)⋅ THEN Auto) }

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  \mforall{}x:E.  ((x  <loc  e)  {}\mRightarrow{}  (before(x)  \mmember{}  \{e':E|  loc(e')  =  loc(x)\}    List))
4.  \mneg{}\muparrow{}first(e)
\mvdash{}  before(pred(e))  \mmember{}  \{e':E|  loc(e')  =  loc(e)\}    List


By

((InstHyp  [pred(e)]  3)\mcdot{}  THEN  Auto)

---

Home Index