---

Step * of Lemma sum-as-accum-filter

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
  (Σ(f[x] | x < n) ~ accumulate (with value x and list item y):
                      x + y
                     over list:
                       filter(λx.(¬b(x =z 0));map(λx.f[x];upto(n)))
                     with starting value:
                      0))
BY
{ ((Auto THEN (RWO "sum-as-accum" 0 THENA Auto)) THEN (GenConclTerm ⌜upto(n)⌝⋅ THENA Auto) THEN Thin (-1)) }

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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (\mSigma{}(f[x]  |  x  <  n)  \msim{}  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];upto(n)))
                                          with  starting  value:
                                            0))


By

---

Latex:
((Auto  THEN  (RWO  "sum-as-accum"  0  THENA  Auto))
  THEN  (GenConclTerm  \mkleeneopen{}upto(n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index