---

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


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. v : A List
5. n : ℕ
6. X : ℕ
⊢ X ≤ accumulate (with value s and list item a):
       #(f[a]) + s
      over list:
        v
      with starting value:
       X + n)
BY
{ (MoveToConcl (-2) THEN ListInd (-2) THEN Reduce 0 THEN Auto')⋅ }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-2)  THEN  ListInd  (-2)  THEN  Reduce  0  THEN  Auto')\mcdot{}

---

Home Index