---

Step * 3 of Lemma bag-bind-append

.....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) ∈ ℙ
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  A  :  Type
2.  B  :  Type
3.  as  :  Base
4.  bs  :  Base
5.  as  =  bs
6.  as  \mmember{}  A  List
7.  bs  \mmember{}  A  List
8.  permutation(A;as;bs)
9.  bb  :  bag(A)
10.  f  :  A  {}\mrightarrow{}  bag(B)
11.  z  :  bag(B)
\mvdash{}  z  =  (bag-bind(bs;f)  +  bag-bind(bb;f))  \mmember{}  \mBbbP{}


By

---

Latex:
Auto

---

Home Index