---

Step * 1 of Lemma bag-combine-size

.....equality..... 
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. as : A List
5. bs : A List
6. permutation(A;as;bs)
⊢ bag-sum(bs;a.#(f[a])) = #(⋃a∈bs.f[a]) ∈ ℕ
BY
{ TACTIC:(ThinVar `as'⋅
          THEN RepUR ``bag-sum bag-size bag-combine bag-map bag-union concat`` 0
          THEN ((ListInd (-1) THEN Reduce 0) THEN Auto)
          THEN Try ((((DoSubsume THEN Auto) THEN BLemma `bag-subtype-list`) THEN Auto)⋅)) }

1
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. u : A
5. v : A List
6. accumulate (with value s and list item a):
    ||f[a]|| + s
   over list:
     v
   with starting value:
    0)
= ||reduce(λl,l'. (l @ l');[];map(λa.f[a];v))||
∈ ℕ
⊢ accumulate (with value s and list item a):
   ||f[a]|| + s
  over list:
    v
  with starting value:
   ||f[u]|| + 0)
= (||f[u]|| + ||reduce(λl,l'. (l @ l');[];map(λa.f[a];v))||)
∈ ℕ

---

Latex:

---

Latex:
.....equality..... 
1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  as  :  A  List
5.  bs  :  A  List
6.  permutation(A;as;bs)
\mvdash{}  bag-sum(bs;a.\#(f[a]))  =  \#(\mcup{}a\mmember{}bs.f[a])


By

---

Latex:
TACTIC:(ThinVar  `as'\mcdot{}
                THEN  RepUR  ``bag-sum  bag-size  bag-combine  bag-map  bag-union  concat``  0
                THEN  ((ListInd  (-1)  THEN  Reduce  0)  THEN  Auto)
                THEN  Try  ((((DoSubsume  THEN  Auto)  THEN  BLemma  `bag-subtype-list`)  THEN  Auto)\mcdot{}))

---

Home Index