---

Step * of Lemma run-system_wf

∀[M:Type ─→ Type]. ∀[r:fulpRunType(P.M[P])]. ∀[t:ℕ+].  (run-system(r;t) ∈ System(P.M[P]))
BY
{ (Unfold `fulpRunType` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:fulpRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].    (run-system(r;t)  \mmember{}  System(P.M[P]))


By

---

Latex:
(Unfold  `fulpRunType`  0  THEN  ProveWfLemma)

---

Home Index