---

Step * of Lemma run-intransit_wf

∀[M:Type ⟶ Type]. ∀[r:pRunType(P.M[P])]. ∀[t:ℕ+].  (run-intransit(r;t) ∈ LabeledDAG(pInTransit(P.M[P])))
BY
{ (RepUR ``pRunType run-intransit run-system`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[t:\mBbbN{}\msupplus{}].
    (run-intransit(r;t)  \mmember{}  LabeledDAG(pInTransit(P.M[P])))


By

---

Latex:
(RepUR  ``pRunType  run-intransit  run-system``  0  THEN  Auto)

---

Home Index