---

Step * of Lemma system-fpf_wf

∀[M:Type ─→ Type]. ∀[S:System(P.M[P])].
  (system-fpf(S) ∈ x:Id fp-> Process(P.M[P]) List × LabeledGraph(pInTransit(P.M[P])))
BY
{ Auto }

1
1. M : Type ─→ Type
2. S : System(P.M[P])
⊢ system-fpf(S) ∈ x:Id fp-> Process(P.M[P]) List × LabeledGraph(pInTransit(P.M[P]))

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index