---

Step * 1 1 2 of Lemma bag-bind-filter


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)
BY
{ AutoSplit }

1
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)
8. ↑p[u]
⊢ (f[u] @ reduce(λl,l'. (l @ l');[];map(λa.f[a];filter(λa.p[a];v))))
= (f[u] @ reduce(λl,l'. (l @ l');[];map(λa.if p[a] then f[a] else [] fi ;v)))
∈ 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.  u  :  A
6.  v  :  A  List
7.  reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}a.f[a];filter(\mlambda{}a.p[a];v)))
=  reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}a.if  p[a]  then  f[a]  else  []  fi  ;v))
\mvdash{}  reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}a.f[a];if  p[u]  then  [u  /  filter(\mlambda{}a.p[a];v)]  else  filter(\mlambda{}a.p[a];v)  \000Cfi  ))
=  (if  p[u]  then  f[u]  else  []  fi    @  reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}a.if  p[a]  then  f[a]  else  []  fi  ;v)\000C))


By

---

Latex:
AutoSplit

---

Home Index