---

Step * of Lemma sum-as-accum

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
  (Σ(f[x] | x < n) ~ accumulate (with value x and list item y):
                      x + y
                     over list:
                       map(λx.f[x];upto(n))
                     with starting value:
                      0))
BY
{ (InductionOnNat
   THEN Auto
   THEN ((RWO "sum-unroll" 0 THENA Auto)
         THEN AutoSplit
         THEN (InstHyp [⌜f⌝] (-3)⋅ THENA Auto)
         THEN (RWO "upto_decomp1" 0 THENA Auto)
         THEN (RWW "map_append_sq list_accum_append" 0 THENA Auto)
         THEN HypSubst (-1) 0
         THEN Reduce 0
         THEN Auto)⋅) }

---

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:
                                              map(\mlambda{}x.f[x];upto(n))
                                          with  starting  value:
                                            0))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  ((RWO  "sum-unroll"  0  THENA  Auto)
              THEN  AutoSplit
              THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
              THEN  (RWO  "upto\_decomp1"  0  THENA  Auto)
              THEN  (RWW  "map\_append\_sq  list\_accum\_append"  0  THENA  Auto)
              THEN  HypSubst  (-1)  0
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index