---

Step * 1 1 1 of Lemma bag-combine-filter

.....equality..... 
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
⊢ ⋃a∈[a∈as|p[a]].f[a] = ⋃a∈as.if p[a] then f[a] else {} fi  ∈ bag(B)
BY
{ (All Thin
   THEN (RepUR ``bag-filter so_lambda`` 0 THEN RepUR ``bag-combine bag-union bag-map empty-bag concat`` 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.  as  :  A  List
6.  bs  :  A  List
7.  permutation(A;as;bs)
8.  as  =  bs
9.  as  \mmember{}  bag(A)
10.  bs  \mmember{}  bag(A)
\mvdash{}  \mcup{}a\mmember{}[a\mmember{}as|p[a]].f[a]  =  \mcup{}a\mmember{}as.if  p[a]  then  f[a]  else  \{\}  fi 


By

---

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

---

Home Index