---

Step * 1 2 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)) ∨ (¬↑(Q u))
⊢ (mapfilter(f;P;v) @ [f u / mapfilter(f;Q;v)])
= [f u / (mapfilter(f;λx.((P x) ∨b(Q x));v) @ 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 Try (Fold `bag-append` 0)
   THEN (InstLemma `bag-append-assoc` [⌈mapfilter(f;P;v)⌉;⌈[f u]⌉;⌈mapfilter(f;Q;v)⌉]⋅ THENA Auto)
   THEN RevHypSubst' (-1) 0
   THEN Try (Fold `cons-bag` 0⋅)
   THEN (InstLemma `bag-append-comm` [⌈U⌉;⌈mapfilter(f;P;v)⌉;⌈f u.[]⌉]⋅ THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN RepUR ``cons-bag bag-append`` 0
   THEN Try (Fold `cons-bag` 0⋅)
   THEN (HypSubst' (-7) 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.  \mneg{}\muparrow{}(P  u)
10.  \muparrow{}(Q  u)
11.  (\muparrow{}(P  u))  \mvee{}  (\muparrow{}(Q  u))
12.  (\mneg{}\muparrow{}(P  u))  \mvee{}  (\mneg{}\muparrow{}(Q  u))
\mvdash{}  (mapfilter(f;P;v)  @  [f  u  /  mapfilter(f;Q;v)])
=  [f  u  /  (mapfilter(f;\mlambda{}x.((P  x)  \mvee{}\msubb{}(Q  x));v)  @  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  Try  (Fold  `bag-append`  0)
  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  RevHypSubst'  (-1)  0
  THEN  Try  (Fold  `cons-bag`  0\mcdot{})
  THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}mapfilter(f;P;v)\mkleeneclose{};\mkleeneopen{}f  u.[]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  RepUR  ``cons-bag  bag-append``  0
  THEN  Try  (Fold  `cons-bag`  0\mcdot{})
  THEN  (HypSubst'  (-7)  0  THENA  Auto)
  THEN  RepUR  ``cons-bag  bag-append``  0
  THEN  Auto)

---

Home Index