---

Step * of Lemma system-function_wf

∀[M:Type ─→ Type]. ∀[S:System(P.M[P])].
  (system-function(S) ∈ Id ─→ (Process(P.M[P]) List × LabeledGraph(pInTransit(P.M[P]))))
BY
{ (ProveWfLemma THEN Fold `lg-nil` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[S:System(P.M[P])].
    (system-function(S)  \mmember{}  Id  {}\mrightarrow{}  (Process(P.M[P])  List  \mtimes{}  LabeledGraph(pInTransit(P.M[P]))))


By

---

Latex:
(ProveWfLemma  THEN  Fold  `lg-nil`  0  THEN  Auto)

---

Home Index