---

Step * of Lemma finite-run-lt

∀[M:Type ─→ Type]
  ∀r:pRunType(P.M[P])
    rel_finite(runEvents(r);run-lt(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)) }

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
⊢ ∃L:runEvents(r) List. ∀z:runEvents(r). ((z run-lt(r) e) ⇒ (z ∈ L))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P])
        rel\_finite(runEvents(r);run-lt(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))

---

Home Index