---

Step * of Lemma well-founded-run-pred

∀[M:Type ─→ Type]
  ∀r:pRunType(P.M[P])
    SWellFounded(x run-pred(r) y) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
BY
{ (InstLemma `run-pred-step-less` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (With ⌈λe.run-event-step(e)⌉ (D 0)⋅ THEN Reduce 0 THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `run-pred-step-less`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (With  \mkleeneopen{}\mlambda{}e.run-event-step(e)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index