Step * 1 of Lemma mapfilter-bor-eq


1. Type@i'
2. Type@i'
3. T ─→ U@i
4. T ─→ 𝔹@i
5. T ─→ 𝔹@i
6. T@i
7. 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 then [u] else [] fi mapfilter(f;P;v)) map(f;if 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 (((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" THENA Auto)
                        THEN RepUR ``cons-bag bag-append`` 0
                        THEN Auto)))) }

1
1. Type@i'
2. Type@i'
3. T ─→ U@i
4. T ─→ 𝔹@i
5. T ─→ 𝔹@i
6. T@i
7. 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 (mapfilter(f;P;v) [f mapfilter(f;Q;v)])]
[f (mapfilter(f;λx.((P x) ∨b(Q x));v) [f mapfilter(f;λx.((P x) ∧b (Q x));v)])]
∈ bag(U)

2
1. Type@i'
2. Type@i'
3. T ─→ U@i
4. T ─→ 𝔹@i
5. T ─→ 𝔹@i
6. T@i
7. 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 mapfilter(f;Q;v)])
[f (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