Step
*
of Lemma
rng_sum_unroll_empty
∀[r:Rng]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) = 0 ∈ |r|) supposing j ≤ i
BY
{ ProveSpecializedLemma `mon_itop_unroll_empty` 1 [parm{i};r↓+gp] (FoldC `rng_sum` ANDTHENC AbReduceC) }
Latex:
Latex:
\mforall{}[r:Rng]. \mforall{}[i,j:\mBbbZ{}]. \mforall{}[E:\{i..j\msupminus{}\} {}\mrightarrow{} |r|]. ((\mSigma{}(r) i \mleq{} k < j. E[k]) = 0) supposing j \mleq{} i
By
Latex:
ProveSpecializedLemma `mon\_itop\_unroll\_empty` 1 [parm\{i\};r\mdownarrow{}+gp] (FoldC `rng\_sum` ANDTHENC AbReduceC)
Home
Index