---

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


1. n : ℕ
2. f : ℕn ⟶ ℤ
3. v : ℕn List
⊢ accumulate (with value x and list item y):
   x + y
  over list:
    map(λx.f[x];v)
  with starting value:
   0)
= 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:
   0)
∈ ℤ
BY
{ ((Assert ⌜∀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)
              ∈ ℤ)⌝⋅
    THEN Try ((BHyp -1  THEN Auto))
    )
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN AutoSplit) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  v  :  \mBbbN{}n  List
\mvdash{}  accumulate  (with  value  x  and  list  item  y):
      x  +  y
    over  list:
        map(\mlambda{}x.f[x];v)
    with  starting  value:
      0)
=  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:
      0)


By

---

Latex:
((Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}
    THEN  Try  ((BHyp  -1    THEN  Auto))
    )
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index