---

Step * 1 1 of Lemma bag-combine-size


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. u : A
5. v : A List
6. accumulate (with value s and list item a):
    ||f[a]|| + s
   over list:
     v
   with starting value:
    0)
= ||reduce(λl,l'. (l @ l');[];map(λa.f[a];v))||
∈ ℕ
⊢ accumulate (with value s and list item a):
   ||f[a]|| + s
  over list:
    v
  with starting value:
   ||f[u]|| + 0)
= (||f[u]|| + ||reduce(λl,l'. (l @ l');[];map(λa.f[a];v))||)
∈ ℕ
BY
{ TACTIC:(RevHypSubst' (-1) 0
          THEN Thin (-1)
          THEN Fold `bag-size` 0
          THEN (GenConcl ⌜#(f[u]) = X ∈ ℕ⌝⋅ THENA Auto)
          THEN (GenConcl ⌜0 = n ∈ ℕ⌝⋅ THENA Auto)
          THEN Thin (-1)
          THEN MoveToConcl (-1)
          THEN (Thin (-1) THEN ListInd (-2))
          THEN Reduce 0
          THEN Auto
          THEN Auto') }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  u  :  A
5.  v  :  A  List
6.  accumulate  (with  value  s  and  list  item  a):
        ||f[a]||  +  s
      over  list:
          v
      with  starting  value:
        0)
=  ||reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}a.f[a];v))||
\mvdash{}  accumulate  (with  value  s  and  list  item  a):
      ||f[a]||  +  s
    over  list:
        v
    with  starting  value:
      ||f[u]||  +  0)
=  (||f[u]||  +  ||reduce(\mlambda{}l,l'.  (l  @  l');[];map(\mlambda{}a.f[a];v))||)


By

---

Latex:
TACTIC:(RevHypSubst'  (-1)  0
                THEN  Thin  (-1)
                THEN  Fold  `bag-size`  0
                THEN  (GenConcl  \mkleeneopen{}\#(f[u])  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}0  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Thin  (-1)
                THEN  MoveToConcl  (-1)
                THEN  (Thin  (-1)  THEN  ListInd  (-2))
                THEN  Reduce  0
                THEN  Auto
                THEN  Auto')

---

Home Index