---

Step * of Lemma decidable__run-lt

∀[M:Type ─→ Type]
  ∀r:pRunType(P.M[P])
    ∀e1,e2:runEvents(r).  Dec(e1 run-lt(r) e2) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
BY
{ (Auto
   THEN Unfold `run-lt` 0
   THEN BLemma `decidable__rel_plus` ⋅
   THEN Auto
   THEN Try ((BLemma `finite-run-pred` THEN Auto))
   THEN Try ((BLemma `well-founded-run-pred` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P])
        \mforall{}e1,e2:runEvents(r).    Dec(e1  run-lt(r)  e2) 
        supposing  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)


By

---

Latex:
(Auto
  THEN  Unfold  `run-lt`  0
  THEN  BLemma  `decidable\_\_rel\_plus`  \mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `finite-run-pred`  THEN  Auto))
  THEN  Try  ((BLemma  `well-founded-run-pred`  THEN  Auto)))

---

Home Index