---

Step * 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
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;S1) ∈ Process(P.M[P]) List
BY
{ (InstLemma `mapfilter_wf` [Id × Process(P.M[P])]⋅ THENA Auto) }

1
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

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  S1  :  (Id  \mtimes{}  Process(P.M[P]))  List
3.  x  :  Id@i
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;S1)  \mmember{}  Process(P.M[P])  List


By

---

Latex:
(InstLemma  `mapfilter\_wf`  [Id  \mtimes{}  Process(P.M[P])]\mcdot{}  THENA  Auto)

---

Home Index