---

Step * 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] ∨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)
BY
{ (RepeatFor 4 (((SplitOnConclITE THENA Auto) THEN Reduce 0))
   THEN RepD
   THEN All (RepUR ``so_apply``)
   THEN Auto
   THEN Try (Complete ((D (-1) THEN Auto)))
   THEN Try (Complete ((D (-2) THEN Auto)))
   THEN Try (Complete ((Try (Fold `cons-bag` 0⋅)
                        THEN (RWO "-5" 0 THENA Auto)
                        THEN RepUR ``cons-bag bag-append`` 0
                        THEN Auto)))) }

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) ∨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)

2
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)

---

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
\mvdash{}  ((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]  \mvee{}\msubb{}Q[u]  then  [u]  else  []  fi  )  @  mapfilter(f;\mlambda{}x.(P[x]  \mvee{}\msubb{}Q[x]);v))
    @  map(f;if  P[u]  \mwedge{}\msubb{}  Q[u]  then  [u]  else  []  fi  )
    @  mapfilter(f;\mlambda{}x.(P[x]  \mwedge{}\msubb{}  Q[x]);v))


By

---

Latex:
(RepeatFor  4  (((SplitOnConclITE  THENA  Auto)  THEN  Reduce  0))
  THEN  RepD
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto
  THEN  Try  (Complete  ((D  (-1)  THEN  Auto)))
  THEN  Try  (Complete  ((D  (-2)  THEN  Auto)))
  THEN  Try  (Complete  ((Try  (Fold  `cons-bag`  0\mcdot{})
                                            THEN  (RWO  "-5"  0  THENA  Auto)
                                            THEN  RepUR  ``cons-bag  bag-append``  0
                                            THEN  Auto))))

---

Home Index