---

Step * 1 of Lemma system-fpf_wf


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]))
BY
{ (D -1
   THEN RepUR ``system-fpf let mkfpf fpf`` 0⋅
   THEN (Assert map(λnd.(snd(fst(fst(nd))));S2) ∈ Id List BY
               ((D -1 THEN Dlg 3) THEN Auto)⋅)) }

1
1. M : Type ⟶ Type
2. S1 : component(P.M[P]) List
3. S2 : LabeledDAG(pInTransit(P.M[P]))
4. map(λnd.(snd(fst(fst(nd))));S2) ∈ Id List
⊢ <remove-repeats(IdDeq;map(λp.(fst(p));S1) @ map(λnd.(snd(fst(fst(nd))));S2))
  , λx.<mapfilter(λc.(snd(c));λc.fst(c) = x;S1), lg-filter(λtr.snd(fst(tr)) = x;S2)>
  > ∈ d:Id List × (x:{x:Id| (x ∈ d)}  ⟶ (Process(P.M[P]) List × LabeledGraph(pInTransit(P.M[P]))))

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1
  THEN  RepUR  ``system-fpf  let  mkfpf  fpf``  0\mcdot{}
  THEN  (Assert  map(\mlambda{}nd.(snd(fst(fst(nd))));S2)  \mmember{}  Id  List  BY
                          ((D  -1  THEN  Dlg  3)  THEN  Auto)\mcdot{}))

---

Home Index