---

Step * of Lemma concat-map-map-decide

∀[T:Type]. ∀[g:Top]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ (Top + Top)].
  (concat(map(λx.map(λy.g[x;y];case f[x] of inl(m) => [m] | inr(x) => []);L)) ~ mapfilter(λx.g[x;outl(f[x])];
                                                                                          λx.isl(f[x]);
                                                                                          L))
BY
{ xxx(Unfold `mapfilter` 0 THEN InductionOnList THEN Reduce 0)xxx }

1
1. T : Type
2. g : Top
⊢ ∀[f:{x:T| (x ∈ [])}  ⟶ (Top + Top)]. ([] ~ [])

2
1. T : Type
2. g : Top
3. u : T
4. v : T List
5. ∀[f:{x:T| (x ∈ v)}  ⟶ (Top + Top)]
     (concat(map(λx.map(λy.g[x;y];case f[x] of inl(m) => [m] | inr(x) => []);v)) 
     ~ map(λx.g[x;outl(f[x])];filter(λx.isl(f[x]);v)))
⊢ ∀[f:{x:T| (x ∈ [u / v])}  ⟶ (Top + Top)]
    (concat([map(λy.g[u;y];case f[u] of inl(m) => [m] | inr(x) => []) / 
             map(λx.map(λy.g[x;y];case f[x] of inl(m) => [m] | inr(x) => []);v)]) ~ map(λx.g[x;outl(f[x])];if isl(f[u])
                                                                                        then [u / 
                                                                                              filter(λx.isl(f[x]);v)]
                                                                                        else filter(λx.isl(f[x]);v)
                                                                                        fi ))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:Top].  \mforall{}[L:T  List].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  (Top  +  Top)].
    (concat(map(\mlambda{}x.map(\mlambda{}y.g[x;y];case  f[x]  of  inl(m)  =>  [m]  |  inr(x)  =>  []);L)) 
    \msim{}  mapfilter(\mlambda{}x.g[x;outl(f[x])];\mlambda{}x.isl(f[x]);L))


By

---

Latex:
xxx(Unfold  `mapfilter`  0  THEN  InductionOnList  THEN  Reduce  0)xxx

---

Home Index