---

Step * 1 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
{ ((GenConclTerm ⌜as⌝⋅ THENA Auto) THEN ThinVar `as' THEN RenameVar `as' (-1) THEN All Thin) }

1
1. A : Type
2. B : Type
3. C : Type
4. f : A ⟶ bag(B)
5. g : B ⟶ bag(C)
6. as : A List@i
⊢ 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:
((GenConclTerm  \mkleeneopen{}as\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `as'  THEN  RenameVar  `as'  (-1)  THEN  All  Thin)

---

Home Index