---

Step * 2 of Lemma bag-combine-append-right


1. A : Type
2. B : Type
3. F : A ⟶ bag(B)
4. G : A ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
⊢ (⋃x∈as.F[x] + ⋃x∈as.G[x]) = (⋃x∈bs.F[x] + ⋃x∈bs.G[x]) ∈ bag(B)
BY
{ (Assert ⌜(as = bs ∈ bag(A)) ∧ (as ∈ bag(A)) ∧ (bs ∈ bag(A))⌝⋅ THEN Auto)⋅ }

1
1. A : Type
2. B : Type
3. F : A ⟶ bag(B)
4. G : A ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
⊢ (⋃x∈as.F[x] + ⋃x∈as.G[x]) = (⋃x∈bs.F[x] + ⋃x∈bs.G[x]) ∈ bag(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  F  :  A  {}\mrightarrow{}  bag(B)
4.  G  :  A  {}\mrightarrow{}  bag(B)
5.  as  :  A  List
6.  bs  :  A  List
7.  permutation(A;as;bs)
\mvdash{}  (\mcup{}x\mmember{}as.F[x]  +  \mcup{}x\mmember{}as.G[x])  =  (\mcup{}x\mmember{}bs.F[x]  +  \mcup{}x\mmember{}bs.G[x])


By

---

Latex:
(Assert  \mkleeneopen{}(as  =  bs)  \mwedge{}  (as  \mmember{}  bag(A))  \mwedge{}  (bs  \mmember{}  bag(A))\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index