---

Step * of Lemma bag-bind-assoc

∀[A,B,C:Type]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)]. ∀[bs:bag(A)].
  (bag-bind(bag-bind(bs;f);g) = bag-bind(bs;λa.bag-bind(f a;g)) ∈ bag(C))
BY
{ TACTIC:(Auto
          THEN RepUR ``bag-bind`` 0
          THEN D -1
          THEN Auto
          THEN RenameVar `as' 6
          THEN RenameVar `bs' 7
          THEN Subst ⌜bag-union(bag-map(g;bag-union(bag-map(f;as))))
                      = bag-union(bag-map(λa.bag-union(bag-map(g;f a));as))
                      ∈ bag(C)⌝ 0⋅
          THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
TACTIC:(Auto
                THEN  RepUR  ``bag-bind``  0
                THEN  D  -1
                THEN  Auto
                THEN  RenameVar  `as'  6
                THEN  RenameVar  `bs'  7
                THEN  Subst  \mkleeneopen{}bag-union(bag-map(g;bag-union(bag-map(f;as))))
                                        =  bag-union(bag-map(\mlambda{}a.bag-union(bag-map(g;f  a));as))\mkleeneclose{}  0\mcdot{}
                THEN  Auto)

---

Home Index