---

Step * 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
⊢ ∃L:runEvents(r) List. ∀z:runEvents(r). ((z run-lt(r) e) ⇒ (z ∈ L))
BY
{ (With ⌈prior-run-events(r;run-event-step(e))⌉ (D 0)⋅ 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
⊢ (z ∈ prior-run-events(r;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
\mvdash{}  \mexists{}L:runEvents(r)  List.  \mforall{}z:runEvents(r).  ((z  run-lt(r)  e)  {}\mRightarrow{}  (z  \mmember{}  L))


By

---

Latex:
(With  \mkleeneopen{}prior-run-events(r;run-event-step(e))\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index