---

Step * 1 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
⊢ run-event-step(z) < run-event-step(e)
BY
{ (BLemma `run-lt-step-less` THEN Auto) }

---

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{}  run-event-step(z)  <  run-event-step(e)


By

---

Latex:
(BLemma  `run-lt-step-less`  THEN  Auto)

---

Home Index