---

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


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. X : ℕ
5. u : A
6. v : A List
7. ∀n:ℕ. (X ≤ accumulate (with value s and list item a): #(f[a]) + sover list:  vwith starting value: X + n))
8. n : ℕ
⊢ X ≤ accumulate (with value s and list item a):
       #(f[a]) + s
      over list:
        v
      with starting value:
       #(f[u]) + X + n)
BY
{ (InstHyp [⌜#(f[u]) + n⌝] (-2)⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(InstHyp  [\mkleeneopen{}\#(f[u])  +  n\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index