---

Step * 2 1 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)))
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 )
BY
{ xxx((((((SplitOnConclITE THENA Auto) THEN Reduce 0 THEN (MoveToConcl (-1)) THEN GenConcl ⌜f[u] = xx ∈ (Top + Top)⌝⋅)
         THENA Auto
         )
        THEN (D (-2))
        THEN Reduce 0
        THEN D 0)
       THENA Auto
       )
      THEN Try (Trivial)
      THEN Try (((D (-1)) THEN Trivial))
      THEN Unfold `concat` 0
      THEN Reduce 0
      THEN Fold `concat` 0
      THEN Try (Trivial)
      THEN EqCD
      THEN Try (Trivial))xxx }

---

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)))
6.  f  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  (Top  +  Top)
7.  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{}  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((((((SplitOnConclITE  THENA  Auto)
                THEN  Reduce  0
                THEN  (MoveToConcl  (-1))
                THEN  GenConcl  \mkleeneopen{}f[u]  =  xx\mkleeneclose{}\mcdot{})
              THENA  Auto
              )
            THEN  (D  (-2))
            THEN  Reduce  0
            THEN  D  0)
          THENA  Auto
          )
        THEN  Try  (Trivial)
        THEN  Try  (((D  (-1))  THEN  Trivial))
        THEN  Unfold  `concat`  0
        THEN  Reduce  0
        THEN  Fold  `concat`  0
        THEN  Try  (Trivial)
        THEN  EqCD
        THEN  Try  (Trivial))xxx

---

Home Index