---

Step * 1 1 of Lemma sum-as-accum-filter


1. n : ℕ
2. f : ℕn ⟶ ℤ
3. u : ℕn
4. v : ℕn List
5. ∀z:ℤ
     (accumulate (with value x and list item y):
       x + y
      over list:
        map(λx.f[x];v)
      with starting value:
       z)
     = accumulate (with value x and list item y):
        x + y
       over list:
         filter(λx.(¬b(x =z 0));map(λx.f[x];v))
       with starting value:
        z)
     ∈ ℤ)
6. z : ℤ
7. f[u] = 0 ∈ ℤ
⊢ accumulate (with value x and list item y):
   x + y
  over list:
    map(λx.f[x];v)
  with starting value:
   z + f[u])
= accumulate (with value x and list item y):
   x + y
  over list:
    filter(λx.(¬b(x =z 0));map(λx.f[x];v))
  with starting value:
   z)
∈ ℤ
BY
{ (RWO "-3<" 0 THEN Auto THEN EqCD THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  u  :  \mBbbN{}n
4.  v  :  \mBbbN{}n  List
5.  \mforall{}z:\mBbbZ{}
          (accumulate  (with  value  x  and  list  item  y):
              x  +  y
            over  list:
                map(\mlambda{}x.f[x];v)
            with  starting  value:
              z)
          =  accumulate  (with  value  x  and  list  item  y):
                x  +  y
              over  list:
                  filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  0));map(\mlambda{}x.f[x];v))
              with  starting  value:
                z))
6.  z  :  \mBbbZ{}
7.  f[u]  =  0
\mvdash{}  accumulate  (with  value  x  and  list  item  y):
      x  +  y
    over  list:
        map(\mlambda{}x.f[x];v)
    with  starting  value:
      z  +  f[u])
=  accumulate  (with  value  x  and  list  item  y):
      x  +  y
    over  list:
        filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  0));map(\mlambda{}x.f[x];v))
    with  starting  value:
      z)


By

---

Latex:
(RWO  "-3<"  0  THEN  Auto  THEN  EqCD  THEN  Auto')

---

Home Index