---

Step * of Lemma first-event-property

∀es:EO. ∀e:E.  (first-event{i:l}(es;e) ≤loc e  ∧ (↑first(first-event{i:l}(es;e))))
BY
{ (Unfold `first-event` 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:


\mforall{}es:EO.  \mforall{}e:E.    (first-event\{i:l\}(es;e)  \mleq{}loc  e    \mwedge{}  (\muparrow{}first(first-event\{i:l\}(es;e))))


By

(Unfold  `first-event`  0  THEN  Auto)

---

Home Index