---

Step * 1 1 1 of Lemma system-fpf_wf

.....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
BY
{ (D (-1) THEN All Thin) }

1
1. M : Type ─→ Type
2. S1 : (Id × Process(P.M[P])) List
3. x : Id@i
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;S1) ∈ Process(P.M[P]) List

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  M  :  Type  {}\mrightarrow{}  Type
2.  S1  :  (Id  \mtimes{}  Process(P.M[P]))  List
3.  S2  :  LabeledDAG(pInTransit(P.M[P]))
4.  map(\mlambda{}nd.(snd(fst(fst(nd))));S2)  \mmember{}  Id  List
5.  x  :  \{x:Id|  (x  \mmember{}  remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));S1)  @  map(\mlambda{}nd.(snd(fst(fst(nd))));S2)))\}  @i
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;S1)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(D  (-1)  THEN  All  Thin)

---

Home Index