---

Step * 1 of Lemma es-first-le


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ↑first(e)
5. loc(e) = loc(e') ∈ Id
6. ¬(e' <loc e)
⊢ e ≤loc e' 
BY
{ (BLemma `es-le-not-locl` THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  \muparrow{}first(e)
5.  loc(e)  =  loc(e')
6.  \mneg{}(e'  <loc  e)
\mvdash{}  e  \mleq{}loc  e' 


By

(BLemma  `es-le-not-locl`  THEN  Auto)

---

Home Index