---

Step * 1 1 1 1 1 2 of Lemma bag-combine-size-bound


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. v : A List
5. n : ℕ
6. z : A
7. X : ℕ
⊢ X ≤ accumulate (with value s and list item a):
       #(f[a]) + s
      over list:
        v
      with starting value:
       #(f[z]) + n) ∈ ℙ
BY
{ (Auto THEN DoSubsume THEN Auto THEN BLemma `bag-subtype-list` THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  v  :  A  List
5.  n  :  \mBbbN{}
6.  z  :  A
7.  X  :  \mBbbN{}
\mvdash{}  X  \mleq{}  accumulate  (with  value  s  and  list  item  a):
              \#(f[a])  +  s
            over  list:
                v
            with  starting  value:
              \#(f[z])  +  n)  \mmember{}  \mBbbP{}


By

---

Latex:
(Auto  THEN  DoSubsume  THEN  Auto  THEN  BLemma  `bag-subtype-list`  THEN  Auto)

---

Home Index