---

Step * of Lemma bag-bind-com

∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ bag(C)]. ∀[ba:bag(A)]. ∀[bb:bag(B)].
  (bag-bind(ba;λa.bag-bind(bb;λb.f[a;b])) = bag-bind(bb;λb.bag-bind(ba;λa.f[a;b])) ∈ bag(C))
BY
{ (Auto THEN RepUR ``bag-bind`` 0 THEN D -1 THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. f : A ⟶ B ⟶ bag(C)
5. ba : bag(A)
6. bb : Base
7. b1 : Base
8. bb = b1 ∈ pertype(λas,bs. ((as ∈ B List) ∧ (bs ∈ B List) ∧ permutation(B;as;bs)))
9. bb ∈ B List
10. b1 ∈ B List
11. permutation(B;bb;b1)
⊢ bag-union(bag-map(λa.bag-union(bag-map(λb.f[a;b];bb));ba))
= bag-union(bag-map(λb.bag-union(bag-map(λa.f[a;b];ba));b1))
∈ bag(C)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[ba:bag(A)].  \mforall{}[bb:bag(B)].
    (bag-bind(ba;\mlambda{}a.bag-bind(bb;\mlambda{}b.f[a;b]))  =  bag-bind(bb;\mlambda{}b.bag-bind(ba;\mlambda{}a.f[a;b])))


By

---

Latex:
(Auto  THEN  RepUR  ``bag-bind``  0  THEN  D  -1  THEN  Auto)

---

Home Index