---

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
{ xxx((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')xxx }

---

Latex:

---

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

---

Latex:
xxx((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')xxx

---

Home Index