---

Step * 1 1 of Lemma finite-run-lt


1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
4. e : runEvents(r)@i
5. z : runEvents(r)@i
6. z run-lt(r) e@i
⊢ (z ∈ prior-run-events(r;run-event-step(e)))
BY
{ (BLemma `member-prior-run-events` THEN Auto) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
4. e : runEvents(r)@i
5. z : runEvents(r)@i
6. z run-lt(r) e@i
⊢ run-event-step(z) < run-event-step(e)

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
3.  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)
4.  e  :  runEvents(r)@i
5.  z  :  runEvents(r)@i
6.  z  run-lt(r)  e@i
\mvdash{}  (z  \mmember{}  prior-run-events(r;run-event-step(e)))


By

---

Latex:
(BLemma  `member-prior-run-events`  THEN  Auto)

---

Home Index