---

Step * 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
6. n : ℕ
7. 0 = n ∈ ℕ
⊢ (a ∈ L) ⇒ (||f[a]|| ≤ accumulate (with value s and list item a): ||f[a]|| + sover list:  Lwith starting value: n))
BY
{ (Thin (-1) THEN MoveToConcl (-1)) }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  L  :  A  List
5.  a  :  A
6.  n  :  \mBbbN{}
7.  0  =  n
\mvdash{}  (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:
(Thin  (-1)  THEN  MoveToConcl  (-1))

---

Home Index