---

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


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)
BY
{ ((RWO "cons_member" (-1) THENM D -1) 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 ∈ A
⊢ #(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.  a  :  A
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}n:\mBbbN{}
          ((a  \mmember{}  v)
          {}\mRightarrow{}  (\#(f[a])  \mleq{}  accumulate  (with  value  s  and  list  item  a):
                                        \#(f[a])  +  s
                                      over  list:
                                          v
                                      with  starting  value:
                                        n)))
8.  n  :  \mBbbN{}
9.  (a  \mmember{}  [u  /  v])
\mvdash{}  \#(f[a])  \mleq{}  accumulate  (with  value  s  and  list  item  a):
                          \#(f[a])  +  s
                        over  list:
                            v
                        with  starting  value:
                          \#(f[u])  +  n)


By

---

Latex:
((RWO  "cons\_member"  (-1)  THENM  D  -1)  THEN  Auto)

---

Home Index