---

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


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. L : A List
5. a : A
⊢ ∀n:ℕ
    ((a ∈ L)
    ⇒ (||f[a]|| ≤ accumulate (with value s and list item a):
                    ||f[a]|| + s
                   over list:
                     L
                   with starting value:
                    n)))
BY
{ (Fold `bag-size` 0 THEN ListInd' (-2) THEN Reduce 0 THEN Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. a : A
5. u : A
6. v : A List
7. ∀n:ℕ
     ((a ∈ v) ⇒ (#(f[a]) ≤ accumulate (with value s and list item a): #(f[a]) + sover list:  vwith starting value: n)))
8. n : ℕ
9. (a ∈ [u / v])
⊢ #(f[a]) ≤ accumulate (with value s and list item a):
             #(f[a]) + s
            over list:
              v
            with starting value:
             #(f[u]) + n)

---

Latex:

---

Latex:

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


By

---

Latex:
(Fold  `bag-size`  0  THEN  ListInd'  (-2)  THEN  Reduce  0  THEN  Auto)

---

Home Index