---

Step * 1 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 ∈ A
⊢ #(f[a]) ≤ accumulate (with value s and list item a):
             #(f[a]) + s
            over list:
              v
            with starting value:
             #(f[u]) + n)
BY
{ (RevHypSubst' (-1) 0 THEN (GenConcl ⌜#(f[a]) = X ∈ ℕ⌝⋅ THENA Auto) THEN All Thin) }

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

2
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. v : A List
5. n : ℕ
6. z : A
7. X : ℕ
⊢ X ≤ accumulate (with value s and list item a):
       #(f[a]) + s
      over list:
        v
      with starting value:
       #(f[z]) + 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  =  u
\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:
(RevHypSubst'  (-1)  0  THEN  (GenConcl  \mkleeneopen{}\#(f[a])  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index