---

Step * of Lemma finite-run-pred

∀[M:Type ⟶ Type]
  ∀r:pRunType(P.M[P])
    rel_finite(runEvents(r);run-pred(r)) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RenameVar`e' (-1)
   THEN With ⌜prior-run-events(r;run-event-step(e))⌝ (D 0)⋅
   THEN Auto
   THEN BLemma `member-prior-run-events`
   THEN Auto
   THEN BLemma `run-pred-step-less`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P])
        rel\_finite(runEvents(r);run-pred(r)) 
        supposing  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar`e'  (-1)
  THEN  With  \mkleeneopen{}prior-run-events(r;run-event-step(e))\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  BLemma  `member-prior-run-events`
  THEN  Auto
  THEN  BLemma  `run-pred-step-less`
  THEN  Auto)

---

Home Index