---

Step * 2 of Lemma concat-map-decide


1. T : Type
2. B : T ⟶ (Top + Top)
3. u : T
4. v : T List
5. concat(map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)
⊢ concat([case B[u] of inl(a) => [a] | inr(a) => [] / map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)]) 
~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);[u / v])
BY
{ xxx(((((((Unfold `mapfilter` 0 THEN Reduce 0 THEN SplitOnConclITE) THENA Auto)
          THEN Reduce 0
          THEN Fold `mapfilter` 0
          THEN (MoveToConcl (-1))
          THEN GenConcl ⌜B[u] = x ∈ (Top + Top)⌝⋅)
         THENA Auto
         )
        THEN (D (-2))
        THEN Reduce 0
        THEN D 0)
       THENA Auto
       )
      THEN Try (Trivial)
      )xxx }

1
1. T : Type
2. B : T ⟶ (Top + Top)
3. u : T
4. v : T List
5. concat(map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)
6. x1 : Top
7. B[u] = (inl x1) ∈ (Top + Top)
8. True
⊢ concat([[x1] / map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)]) ~ [x1 / mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)]

2
1. T : Type
2. B : T ⟶ (Top + Top)
3. u : T
4. v : T List
5. concat(map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)
6. y : Top
7. B[u] = (inr y ) ∈ (Top + Top)
8. ¬False
⊢ concat([[] / map(λx.case B[x] of inl(a) => [a] | inr(a) => [];v)]) ~ mapfilter(λx.outl(B[x]);λx.isl(B[x]);v)

---

Latex:

---

Latex:

1.  T  :  Type
2.  B  :  T  {}\mrightarrow{}  (Top  +  Top)
3.  u  :  T
4.  v  :  T  List
5.  concat(map(\mlambda{}x.case  B[x]  of  inl(a)  =>  [a]  |  inr(a)  =>  [];v))  \msim{}  mapfilter(\mlambda{}x.outl(B[x]);
                                                                                                                                                      \mlambda{}x.isl(B[x]);
                                                                                                                                                      v)
\mvdash{}  concat([case  B[u]  of  inl(a)  =>  [a]  |  inr(a)  =>  []  / 
                    map(\mlambda{}x.case  B[x]  of  inl(a)  =>  [a]  |  inr(a)  =>  [];v)])  \msim{}  mapfilter(\mlambda{}x.outl(B[x]);
                                                                                                                                                        \mlambda{}x.isl(B[x]);
                                                                                                                                                        [u  /  v])


By

---

Latex:
xxx(((((((Unfold  `mapfilter`  0  THEN  Reduce  0  THEN  SplitOnConclITE)  THENA  Auto)
                THEN  Reduce  0
                THEN  Fold  `mapfilter`  0
                THEN  (MoveToConcl  (-1))
                THEN  GenConcl  \mkleeneopen{}B[u]  =  x\mkleeneclose{}\mcdot{})
              THENA  Auto
              )
            THEN  (D  (-2))
            THEN  Reduce  0
            THEN  D  0)
          THENA  Auto
          )
        THEN  Try  (Trivial)
        )xxx

---

Home Index