---

Step * 1 of Lemma bag-bind-filter


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 ;b2)) ∈ bag(B)
BY
{ Subst ⌜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)⌝ 0
⋅ }

1
.....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)

2
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.if p[a] then f[a] else {} fi ;b1))
= bag-union(bag-map(λa.if p[a] then f[a] else {} fi ;b2))
∈ bag(B)

3
.....wf..... 
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)
8. z : bag(B)
⊢ z = bag-union(bag-map(λa.if p[a] then f[a] else {} fi ;b2)) ∈ bag(B) ∈ ℙ

---

Latex:

---

Latex:

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  ;b2))


By

---

Latex:
Subst  \mkleeneopen{}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))\mkleeneclose{}  0\mcdot{}

---

Home Index