---

Step * 1 1 of Lemma bag-bind-append


1. A : Type
2. B : Type
3. bb : bag(A)
4. f : A ⟶ bag(B)
5. as : A List
⊢ bag-bind(as + bb;f) = (bag-bind(as;f) + bag-bind(bb;f)) ∈ bag(B)
BY
{ (ListInd (-1)
   THEN RepUR ``bag-append bag-bind bag-map bag-union concat`` 0
   THEN Fold `concat` 0
   THEN Folds ``bag-map bag-union`` 0
   THEN Folds ``bag-bind bag-append`` 0)⋅ }

1
1. A : Type
2. B : Type
3. bb : bag(A)
4. f : A ⟶ bag(B)
⊢ bag-bind(bb;f) = bag-bind(bb;f) ∈ bag(B)

2
1. A : Type
2. B : Type
3. bb : bag(A)
4. f : A ⟶ bag(B)
5. u : A
6. v : A List
7. bag-bind(v + bb;f) = (bag-bind(v;f) + bag-bind(bb;f)) ∈ bag(B)
⊢ ((f u) + bag-bind(v + bb;f)) = (((f u) + bag-bind(v;f)) + bag-bind(bb;f)) ∈ bag(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  bb  :  bag(A)
4.  f  :  A  {}\mrightarrow{}  bag(B)
5.  as  :  A  List
\mvdash{}  bag-bind(as  +  bb;f)  =  (bag-bind(as;f)  +  bag-bind(bb;f))


By

---

Latex:
(ListInd  (-1)
  THEN  RepUR  ``bag-append  bag-bind  bag-map  bag-union  concat``  0
  THEN  Fold  `concat`  0
  THEN  Folds  ``bag-map  bag-union``  0
  THEN  Folds  ``bag-bind  bag-append``  0)\mcdot{}

---

Home Index