---

Step * of Lemma bag-bind-append

∀[A,B:Type]. ∀[ba,bb:bag(A)]. ∀[f:A ⟶ bag(B)].  (bag-bind(ba + bb;f) = (bag-bind(ba;f) + bag-bind(bb;f)) ∈ bag(B))
BY
{ (Auto
   THEN D -3
   THEN Auto
   THEN RenameVar `as' 3
   THEN RenameVar `bs' 4
   THEN Subst ⌜bag-bind(as + bb;f) = (bag-bind(as;f) + bag-bind(bb;f)) ∈ bag(B)⌝ 0⋅) }

1
.....equality..... 
1. A : Type
2. B : Type
3. as : Base
4. bs : Base
5. as = bs ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. as ∈ A List
7. bs ∈ A List
8. permutation(A;as;bs)
9. bb : bag(A)
10. f : A ⟶ bag(B)
⊢ bag-bind(as + bb;f) = (bag-bind(as;f) + bag-bind(bb;f)) ∈ bag(B)

2
1. A : Type
2. B : Type
3. as : Base
4. bs : Base
5. as = bs ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. as ∈ A List
7. bs ∈ A List
8. permutation(A;as;bs)
9. bb : bag(A)
10. f : A ⟶ bag(B)
⊢ (bag-bind(as;f) + bag-bind(bb;f)) = (bag-bind(bs;f) + bag-bind(bb;f)) ∈ bag(B)

3
.....wf..... 
1. A : Type
2. B : Type
3. as : Base
4. bs : Base
5. as = bs ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
6. as ∈ A List
7. bs ∈ A List
8. permutation(A;as;bs)
9. bb : bag(A)
10. f : A ⟶ bag(B)
11. z : bag(B)
⊢ z = (bag-bind(bs;f) + bag-bind(bb;f)) ∈ bag(B) ∈ ℙ

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -3
  THEN  Auto
  THEN  RenameVar  `as'  3
  THEN  RenameVar  `bs'  4
  THEN  Subst  \mkleeneopen{}bag-bind(as  +  bb;f)  =  (bag-bind(as;f)  +  bag-bind(bb;f))\mkleeneclose{}  0\mcdot{})

---

Home Index