---

Step * 1 1 of Lemma mapfilter-bor-eq


1. T : Type@i'
2. U : Type@i'
3. f : T ─→ U@i
4. P : T ─→ 𝔹@i
5. Q : T ─→ 𝔹@i
6. u : T@i
7. v : T List@i
8. (mapfilter(f;P;v) @ mapfilter(f;Q;v))
= (mapfilter(f;λx.((P x) ∨b(Q x));v) @ mapfilter(f;λx.((P x) ∧b (Q x));v))
∈ bag(U)@i
9. ↑(P u)
10. ↑(Q u)
11. (↑(P u)) ∨ (↑(Q u))
12. ↑(P u)
13. ↑(Q u)
⊢ [f u / (mapfilter(f;P;v) @ [f u / mapfilter(f;Q;v)])]
= [f u / (mapfilter(f;λx.((P x) ∨b(Q x));v) @ [f u / mapfilter(f;λx.((P x) ∧b (Q x));v)])]
∈ bag(U)
BY
{ ((Subst ⌈[f u / mapfilter(f;Q;v)] ~ [f u] @ mapfilter(f;Q;v)⌉ 0⋅ THENA (Reduce 0 THEN Auto))
   THEN (Subst ⌈[f u / (mapfilter(f;P;v) @ [f u] @ mapfilter(f;Q;v))] ~ [f u]
                @ mapfilter(f;P;v)
                @ [f u]
                @ mapfilter(f;Q;v)⌉ 0⋅
         THENA (Reduce 0 THEN Auto)
         )
   THEN (Subst ⌈[f u / mapfilter(f;λx.((P x) ∧b (Q x));v)] ~ [f u] @ mapfilter(f;λx.((P x) ∧b (Q x));v)⌉ 0⋅
         THENA (Reduce 0 THEN Auto)
         )
   THEN ((InstLemma `bag-append-assoc` [⌈mapfilter(f;P;v)⌉;⌈[f u]⌉;⌈mapfilter(f;Q;v)⌉]⋅ THENA Auto)
         THEN Try (Fold `bag-append` 0)
         THEN RevHypSubst' (-1) 0
         THEN Thin (-1)
         THEN Try (Fold `cons-bag` 0)
         THEN (InstLemma `bag-append-assoc` [⌈mapfilter(f;λx.((P x) ∨b(Q x));v)⌉;⌈f u.[]⌉;⌈mapfilter(f;
                                                                                                     λx.((P x)
                                                                                                        ∧b (Q x));
                                                                                                     v)⌉]⋅
               THENA Auto
               )
         THEN RevHypSubst' (-1) 0
         THEN Thin (-1)
         THEN (InstLemma `bag-append-comm` [⌈U⌉;⌈f u.[]⌉;⌈mapfilter(f;P;v)⌉]⋅ THENA Auto)
         THEN (RevHypSubst' (-1) 0 THENA Auto)
         THEN Thin (-1)
         THEN (InstLemma `bag-append-comm` [⌈U⌉;⌈f u.[]⌉;⌈mapfilter(f;λx.((P x) ∨b(Q x));v)⌉]⋅ THENA Auto)
         THEN (RevHypSubst' (-1) 0 THENA Auto)
         THEN Thin (-1)
         THEN (InstLemma `bag-append-assoc` [⌈f u.[]⌉;⌈mapfilter(f;P;v)⌉;⌈mapfilter(f;Q;v)⌉]⋅ THENA Auto)
         THEN HypSubst' (-1) 0
         THEN Thin (-1)
         THEN Try (Fold `bag-append` (-6))
         THEN (HypSubst' (-6) 0 THENA Auto)
         THEN RepUR ``cons-bag bag-append`` 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  U  :  Type@i'
3.  f  :  T  {}\mrightarrow{}  U@i
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}@i
5.  Q  :  T  {}\mrightarrow{}  \mBbbB{}@i
6.  u  :  T@i
7.  v  :  T  List@i
8.  (mapfilter(f;P;v)  @  mapfilter(f;Q;v))
=  (mapfilter(f;\mlambda{}x.((P  x)  \mvee{}\msubb{}(Q  x));v)  @  mapfilter(f;\mlambda{}x.((P  x)  \mwedge{}\msubb{}  (Q  x));v))@i
9.  \muparrow{}(P  u)
10.  \muparrow{}(Q  u)
11.  (\muparrow{}(P  u))  \mvee{}  (\muparrow{}(Q  u))
12.  \muparrow{}(P  u)
13.  \muparrow{}(Q  u)
\mvdash{}  [f  u  /  (mapfilter(f;P;v)  @  [f  u  /  mapfilter(f;Q;v)])]
=  [f  u  /  (mapfilter(f;\mlambda{}x.((P  x)  \mvee{}\msubb{}(Q  x));v)  @  [f  u  /  mapfilter(f;\mlambda{}x.((P  x)  \mwedge{}\msubb{}  (Q  x));v)])]


By

---

Latex:
((Subst  \mkleeneopen{}[f  u  /  mapfilter(f;Q;v)]  \msim{}  [f  u]  @  mapfilter(f;Q;v)\mkleeneclose{}  0\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  (Subst  \mkleeneopen{}[f  u  /  (mapfilter(f;P;v)  @  [f  u]  @  mapfilter(f;Q;v))]  \msim{}  [f  u]
                            @  mapfilter(f;P;v)
                            @  [f  u]
                            @  mapfilter(f;Q;v)\mkleeneclose{}  0\mcdot{}
              THENA  (Reduce  0  THEN  Auto)
              )
  THEN  (Subst  \mkleeneopen{}[f  u  /  mapfilter(f;\mlambda{}x.((P  x)  \mwedge{}\msubb{}  (Q  x));v)]  \msim{}  [f  u]
                            @  mapfilter(f;\mlambda{}x.((P  x)  \mwedge{}\msubb{}  (Q  x));v)\mkleeneclose{}  0\mcdot{}
              THENA  (Reduce  0  THEN  Auto)
              )
  THEN  ((InstLemma  `bag-append-assoc`  [\mkleeneopen{}mapfilter(f;P;v)\mkleeneclose{};\mkleeneopen{}[f  u]\mkleeneclose{};\mkleeneopen{}mapfilter(f;Q;v)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  Try  (Fold  `bag-append`  0)
              THEN  RevHypSubst'  (-1)  0
              THEN  Thin  (-1)
              THEN  Try  (Fold  `cons-bag`  0)
              THEN  (InstLemma  `bag-append-assoc`  [\mkleeneopen{}mapfilter(f;\mlambda{}x.((P  x)  \mvee{}\msubb{}(Q  x));v)\mkleeneclose{};\mkleeneopen{}f  u.[]\mkleeneclose{};
                          \mkleeneopen{}mapfilter(f;\mlambda{}x.((P  x)  \mwedge{}\msubb{}  (Q  x));v)\mkleeneclose{}]\mcdot{}
                          THENA  Auto
                          )
              THEN  RevHypSubst'  (-1)  0
              THEN  Thin  (-1)
              THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}f  u.[]\mkleeneclose{};\mkleeneopen{}mapfilter(f;P;v)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
              THEN  Thin  (-1)
              THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}f  u.[]\mkleeneclose{};\mkleeneopen{}mapfilter(f;\mlambda{}x.((P  x)  \mvee{}\msubb{}(Q  x));v)\mkleeneclose{}]\mcdot{}
                          THENA  Auto
                          )
              THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
              THEN  Thin  (-1)
              THEN  (InstLemma  `bag-append-assoc`  [\mkleeneopen{}f  u.[]\mkleeneclose{};\mkleeneopen{}mapfilter(f;P;v)\mkleeneclose{};\mkleeneopen{}mapfilter(f;Q;v)\mkleeneclose{}]\mcdot{}
                          THENA  Auto
                          )
              THEN  HypSubst'  (-1)  0
              THEN  Thin  (-1)
              THEN  Try  (Fold  `bag-append`  (-6))
              THEN  (HypSubst'  (-6)  0  THENA  Auto)
              THEN  RepUR  ``cons-bag  bag-append``  0
              THEN  Auto)\mcdot{})

---

Home Index