---

Step * 1 1 of Lemma bag-sum-count


1. A : Type
2. B : Type
3. f : B ⟶ bag(A)
4. eq : EqDecider(A)
5. z : A
6. bs : B List
7. ¬(1 ≤ (#z in f[last(bs)]))
8. ¬↑null(bs)
9. ||bs|| ≥ 1 
10. accumulate (with value s and list item b):
     (#z in f[b]) + s
    over list:
      firstn(||bs|| - 1;bs)
    with starting value:
     0)
= accumulate (with value s and list item b):
   (#z in f[b]) + s
  over list:
    filter(λb.1 ≤z (#z in f[b]);firstn(||bs|| - 1;bs))
  with starting value:
   0)
∈ ℤ
11. v : ℤ
12. accumulate (with value s and list item b):
     (#z in f[b]) + s
    over list:
      firstn(||bs|| - 1;bs)
    with starting value:
     0)
= v
∈ ℤ
⊢ ((#z in f[last(bs)]) + v) = v ∈ ℤ
BY
{ xxx(Subst ⌜(#z in f[last(bs)]) ~ 0⌝ 0⋅ THEN Auto')⋅xxx }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  B  {}\mrightarrow{}  bag(A)
4.  eq  :  EqDecider(A)
5.  z  :  A
6.  bs  :  B  List
7.  \mneg{}(1  \mleq{}  (\#z  in  f[last(bs)]))
8.  \mneg{}\muparrow{}null(bs)
9.  ||bs||  \mgeq{}  1 
10.  accumulate  (with  value  s  and  list  item  b):
          (\#z  in  f[b])  +  s
        over  list:
            firstn(||bs||  -  1;bs)
        with  starting  value:
          0)
=  accumulate  (with  value  s  and  list  item  b):
      (\#z  in  f[b])  +  s
    over  list:
        filter(\mlambda{}b.1  \mleq{}z  (\#z  in  f[b]);firstn(||bs||  -  1;bs))
    with  starting  value:
      0)
11.  v  :  \mBbbZ{}
12.  accumulate  (with  value  s  and  list  item  b):
          (\#z  in  f[b])  +  s
        over  list:
            firstn(||bs||  -  1;bs)
        with  starting  value:
          0)
=  v
\mvdash{}  ((\#z  in  f[last(bs)])  +  v)  =  v


By

---

Latex:
xxx(Subst  \mkleeneopen{}(\#z  in  f[last(bs)])  \msim{}  0\mkleeneclose{}  0\mcdot{}  THEN  Auto')\mcdot{}xxx

---

Home Index