---

Step * of Lemma mapfilter-bor-eq

∀T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
  ((mapfilter(f;P;L) @ mapfilter(f;Q;L))
  = (mapfilter(f;λx.(P[x] ∨bQ[x]);L) @ mapfilter(f;λx.(P[x] ∧b Q[x]);L))
  ∈ bag(U))
BY
{ ((UnivCD THENA Auto)
   THEN ListInd (-1)
   THEN Try (Complete ((RepUR ``mapfilter filter`` 0 THEN Auto)))
   THEN (Subst ⌜[u / v] ~ [u] @ v⌝ 0⋅ THENA (Reduce 0 THEN Auto))
   THEN (RWO "mapfilter-append" 0 THENA Auto)
   THEN (RWO "mapfilter-singleton" 0 THENA Auto)
   THEN Reduce 0) }

1
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] ∨bQ[x]);v) @ mapfilter(f;λx.(P[x] ∧b Q[x]);v))
∈ bag(U)@i
⊢ ((map(f;if P u then [u] else [] fi ) @ mapfilter(f;P;v)) @ map(f;if Q u then [u] else [] fi ) @ mapfilter(f;Q;v))
= ((map(f;if P[u] ∨bQ[u] then [u] else [] fi ) @ mapfilter(f;λx.(P[x] ∨bQ[x]);v))
  @ map(f;if P[u] ∧b Q[u] then [u] else [] fi )
  @ mapfilter(f;λx.(P[x] ∧b Q[x]);v))
∈ bag(U)

---

Latex:

---

Latex:
\mforall{}T,U:Type.  \mforall{}f:T  {}\mrightarrow{}  U.  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
    ((mapfilter(f;P;L)  @  mapfilter(f;Q;L))
    =  (mapfilter(f;\mlambda{}x.(P[x]  \mvee{}\msubb{}Q[x]);L)  @  mapfilter(f;\mlambda{}x.(P[x]  \mwedge{}\msubb{}  Q[x]);L)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ListInd  (-1)
  THEN  Try  (Complete  ((RepUR  ``mapfilter  filter``  0  THEN  Auto)))
  THEN  (Subst  \mkleeneopen{}[u  /  v]  \msim{}  [u]  @  v\mkleeneclose{}  0\mcdot{}  THENA  (Reduce  0  THEN  Auto))
  THEN  (RWO  "mapfilter-append"  0  THENA  Auto)
  THEN  (RWO  "mapfilter-singleton"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index