---

Step * of Lemma bag-bind-filter

∀[A,B:Type]. ∀[p:A ⟶ 𝔹]. ∀[f:{a:A| ↑p[a]}  ⟶ bag(B)]. ∀[ba:bag(A)].
  (bag-bind([a∈ba|p[a]];λa.f[a]) = bag-bind(ba;λa.if p[a] then f[a] else {} fi ) ∈ bag(B))
BY
{ (Auto
   THEN RepUR ``bag-bind`` 0
   THEN D -1
   THEN Auto
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜ba⌝;⌜b1⌝]⋅
   THEN All Thin
   THEN RenameVar `b1' (-2)
   THEN RenameVar `b2' (-1)
   THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[p:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{a:A|  \muparrow{}p[a]\}    {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].
    (bag-bind([a\mmember{}ba|p[a]];\mlambda{}a.f[a])  =  bag-bind(ba;\mlambda{}a.if  p[a]  then  f[a]  else  \{\}  fi  ))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-bind``  0
  THEN  D  -1
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}ba\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  RenameVar  `b1'  (-2)
  THEN  RenameVar  `b2'  (-1)
  THEN  Auto)

---

Home Index