---

Step * 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. (a ∈ L)
7. L ∈ bag(A)
⊢ #(f[a]) ≤ bag-sum(L;a.#(f[a]))
BY
{ (Thin (-1) THEN MoveToConcl (-1) THEN RepUR ``bag-size bag-sum`` 0 THEN (GenConcl ⌜0 = n ∈ ℕ⌝⋅ THENA Auto)) }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  L  :  A  List
5.  a  :  A
6.  (a  \mmember{}  L)
7.  L  \mmember{}  bag(A)
\mvdash{}  \#(f[a])  \mleq{}  bag-sum(L;a.\#(f[a]))


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``bag-size  bag-sum``  0
  THEN  (GenConcl  \mkleeneopen{}0  =  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index