---

Step * of Lemma the-first-event

∀es:EO. ∀e:E.  ∃x:E. (x ≤loc e  ∧ (↑first(x)))
BY
{ (Auto THEN With ⌜es-init(es;e)⌝ (D 0)⋅ THEN Auto) }

1
1. es : EO@i'
2. e : E@i
⊢ es-init(es;e) ≤loc e 

2
1. es : EO@i'
2. e : E@i
3. es-init(es;e) ≤loc e 
⊢ ↑first(es-init(es;e))

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e:E.    \mexists{}x:E.  (x  \mleq{}loc  e    \mwedge{}  (\muparrow{}first(x)))


By

---

Latex:
(Auto  THEN  With  \mkleeneopen{}es-init(es;e)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index