---

Step * of Lemma qsum_unroll

∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ].  (Σa ≤ j < b. E[j] ~ if a <z b then Σa ≤ j < b - 1. E[j] + E[b - 1] else 0 fi )
BY
{ (RepUR ``qsum rng_sum mon_itop`` 0
   THEN (UnivCD THENA Auto)
   THEN RW (AddrC [1] RecUnfoldTopAbC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].
    (\mSigma{}a  \mleq{}  j  <  b.  E[j]  \msim{}  if  a  <z  b  then  \mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  +  E[b  -  1]  else  0  fi  )


By

---

Latex:
(RepUR  ``qsum  rng\_sum  mon\_itop``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index