---

Step * 2 of Lemma concat-map-map-decide


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 ))
BY
{ xxx(((D 0 THENA Auto) THEN (InstHyp [⌜f⌝] (-2))⋅) THENA Auto)xxx }

1
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)))
6. f : {x:T| (x ∈ [u / v])}  ⟶ (Top + Top)
7. 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))
⊢ 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:

1.  T  :  Type
2.  g  :  Top
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[f:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  (Top  +  Top)]
          (concat(map(\mlambda{}x.map(\mlambda{}y.g[x;y];case  f[x]  of  inl(m)  =>  [m]  |  inr(x)  =>  []);v)) 
          \msim{}  map(\mlambda{}x.g[x;outl(f[x])];filter(\mlambda{}x.isl(f[x]);v)))
\mvdash{}  \mforall{}[f:\{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  (Top  +  Top)]
        (concat([map(\mlambda{}y.g[u;y];case  f[u]  of  inl(m)  =>  [m]  |  inr(x)  =>  [])  / 
                          map(\mlambda{}x.map(\mlambda{}y.g[x;y];case  f[x]  of  inl(m)  =>  [m]  |  inr(x)  =>  []);v)]) 
        \msim{}  map(\mlambda{}x.g[x;outl(f[x])];if  isl(f[u])
                    then  [u  /  filter(\mlambda{}x.isl(f[x]);v)]
                    else  filter(\mlambda{}x.isl(f[x]);v)
                    fi  ))


By

---

Latex:
xxx(((D  0  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-2))\mcdot{})  THENA  Auto)xxx

---

Home Index