---

Step * of Lemma rv-partial-sum-unroll

∀[m:ℕ+]. ∀[X:Top].  (rv-partial-sum(m;i.X[i]) ~ rv-partial-sum(m - 1;i.X[i]) + X[m - 1])
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``rv-add rv-partial-sum qsum rng_sum mon_itop`` 0
   THEN (RW (AddrC [1] (RecUnfoldC `itop`)) 0)
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0
   THEN Try (Trivial)
   THEN Auto') }

---

Latex:


\mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[X:Top].    (rv-partial-sum(m;i.X[i])  \msim{}  rv-partial-sum(m  -  1;i.X[i])  +  X[m  -  1])


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``rv-add  rv-partial-sum  qsum  rng\_sum  mon\_itop``  0
  THEN  (RW  (AddrC  [1]  (RecUnfoldC  `itop`))  0)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  Auto')

---

Home Index