---

Step * 2 of Lemma the-first-event


1. es : EO@i'
2. e : E@i
3. es-init(es;e) ≤loc e 
⊢ ↑first(es-init(es;e))
BY
{ (RWO "es-first-init" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "es-first-init"  0  THEN  Auto)\mcdot{}

---

Home Index