---

Step * 1 1 of Lemma system-fpf_wf


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]))))
BY
{ (Unfold `component` 2 THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto))))) }

1
.....subterm..... T:t
1:n
1. M : Type ⟶ Type
2. S1 : (Id × Process(P.M[P])) List
3. S2 : LabeledDAG(pInTransit(P.M[P]))
4. map(λnd.(snd(fst(fst(nd))));S2) ∈ Id List
5. x : {x:Id| (x ∈ remove-repeats(IdDeq;map(λp.(fst(p));S1) @ map(λnd.(snd(fst(fst(nd))));S2)))} @i
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;S1) ∈ Process(P.M[P]) List

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `component`  2  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto)))))

---

Home Index