---

Step * of Lemma prior-run-events_wf

∀[M:Type ⟶ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ].  (prior-run-events(r;t) ∈ runEvents(r) List)
BY
{ ProveWfLemma }

1
1. M : Type ⟶ Type
2. r : pRunType(P.M[P])
3. t : ℕ
4. ∀x:ℕ. (↑((λt.isl(fst((r t)))) x) ∈ Type)
5. t1 : ℕ@i
6. ↑((λt.isl(fst((r t)))) t1)@i
⊢ <t1, fst(snd(outl(fst((r t1)))))> ∈ runEvents(r)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[t:\mBbbN{}].    (prior-run-events(r;t)  \mmember{}  runEvents(r)  List)


By

---

Latex:
ProveWfLemma

---

Home Index