---

Step * 1 of Lemma es-init-le-iff


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e') = loc(e) ∈ Id@i
5. es-init(es;e') = es-init(es;e) ∈ E
⊢ es-init(es;e') ≤loc e' 
BY
{ (BLemma `es-init-le` THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  loc(e')  =  loc(e)@i
5.  es-init(es;e')  =  es-init(es;e)
\mvdash{}  es-init(es;e')  \mleq{}loc  e' 


By

(BLemma  `es-init-le`  THEN  Auto)

---

Home Index