---

Step * of Lemma sum_unroll_lo_q

No Annotations
∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = (E[i] + Σi + 1 ≤ k < j. E[k]) ∈ ℚ) supposing i < j
BY
{ ((ProveSpecializedLemmaWReduce rng_sum_unroll_lo) 0 [⌜parm{i}⌝; ⌜<ℚ+*>⌝]⋅ THEN Fold `qsum` (-1) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((ProveSpecializedLemmaWReduce  rng\_sum\_unroll\_lo)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};  \mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}
  THEN  Fold  `qsum`  (-1)
  THEN  Auto)

---

Home Index