---

Step * 2 of Lemma first-event-property


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:



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


By

(RWO  "es-first-init"  0  THEN  Auto)

---

Home Index