---

Step * 1 of Lemma bag-bind-assoc

.....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)
BY
{ (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:
.....equality..... 
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  A  {}\mrightarrow{}  bag(B)
5.  g  :  B  {}\mrightarrow{}  bag(C)
6.  as  :  Base
7.  bs  :  Base
8.  as  =  bs
9.  as  \mmember{}  A  List
10.  bs  \mmember{}  A  List
11.  permutation(A;as;bs)
\mvdash{}  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))


By

---

Latex:
(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