---

Step * of Lemma rng_sum_single

∀[r:Rng]. ∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = E[i] ∈ |r|) supposing j = (i + 1) ∈ ℤ
BY
{ (InstLemma `rng_sum_unroll_lo` []
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))
   THEN NthHypEqTrans (-1)
   THEN RWO "rng_sum_unroll_base" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[i,j:\mBbbZ{}].    \mforall{}[E:\{i..j\msupminus{}\}  {}\mrightarrow{}  |r|].  ((\mSigma{}(r)  i  \mleq{}  k  <  j.  E[k])  =  E[i])  supposing  j  =  (i  +  1)


By

---

Latex:
(InstLemma  `rng\_sum\_unroll\_lo`  []
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  NthHypEqTrans  (-1)
  THEN  RWO  "rng\_sum\_unroll\_base"  0
  THEN  Auto)

---

Home Index