---

Step * 1 1 1 1 1 of Lemma system-fpf_wf


1. M : Type ─→ Type
2. S1 : (Id × Process(P.M[P])) List
3. x : Id@i
4. ∀[L:(Id × Process(P.M[P])) List]. ∀[P:(Id × Process(P.M[P])) ─→ 𝔹]. ∀[T':Type].
   ∀[f:{x:Id × Process(P.M[P])| ↑(P x)}  ─→ T'].
     (mapfilter(f;P;L) ∈ T' List)
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;S1) ∈ Process(P.M[P]) List
BY
{ (BHyp (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  S1  :  (Id  \mtimes{}  Process(P.M[P]))  List
3.  x  :  Id@i
4.  \mforall{}[L:(Id  \mtimes{}  Process(P.M[P]))  List].  \mforall{}[P:(Id  \mtimes{}  Process(P.M[P]))  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[T':Type].
      \mforall{}[f:\{x:Id  \mtimes{}  Process(P.M[P])|  \muparrow{}(P  x)\}    {}\mrightarrow{}  T'].
          (mapfilter(f;P;L)  \mmember{}  T'  List)
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;S1)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(BHyp  (-1)  THEN  Auto)

---

Home Index