---

Step * 1 1 of Lemma bag-bind-filter

.....equality..... 
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. b1 : A List
6. b2 : A List
7. permutation(A;b1;b2)
⊢ bag-union(bag-map(λa.f[a];[a∈b1|p[a]])) = bag-union(bag-map(λa.if p[a] then f[a] else {} fi ;b1)) ∈ bag(B)
BY
{ (All Thin THEN RepUR ``bag-union bag-map empty-bag concat bag-filter`` 0 THEN ListInd (-1)⋅ THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
⊢ [] = [] ∈ bag(B)

2
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. u : A
6. v : A List
7. reduce(λl,l'. (l @ l');[];map(λa.f[a];filter(λa.p[a];v)))
= reduce(λl,l'. (l @ l');[];map(λa.if p[a] then f[a] else [] fi ;v))
∈ bag(B)
⊢ reduce(λl,l'. (l @ l');[];map(λa.f[a];if p[u] then [u / filter(λa.p[a];v)] else filter(λa.p[a];v) fi ))
= (if p[u] then f[u] else [] fi  @ reduce(λl,l'. (l @ l');[];map(λa.if p[a] then f[a] else [] fi ;v)))
∈ bag(B)

---

Latex:

---

Latex:
.....equality..... 
1.  A  :  Type
2.  B  :  Type
3.  p  :  A  {}\mrightarrow{}  \mBbbB{}
4.  f  :  \{a:A|  \muparrow{}p[a]\}    {}\mrightarrow{}  bag(B)
5.  b1  :  A  List
6.  b2  :  A  List
7.  permutation(A;b1;b2)
\mvdash{}  bag-union(bag-map(\mlambda{}a.f[a];[a\mmember{}b1|p[a]]))  =  bag-union(bag-map(\mlambda{}a.if  p[a]  then  f[a]  else  \{\}  fi  ;b1))


By

---

Latex:
(All  Thin
  THEN  RepUR  ``bag-union  bag-map  empty-bag  concat  bag-filter``  0
  THEN  ListInd
  (-1)\mcdot{}
  THEN  Reduce  0)

---

Home Index