---

Step * of Lemma rsum_unroll

No Annotations
∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ].
  (Σ{x[k] | n≤k≤m} = if m <z n then r0 if (m =z n) then x[n] else Σ{x[k] | n≤k≤m - 1} + x[m] fi )
BY
{ (Auto
   THEN Unfold `rsum` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Repeat (AutoSplit)
   THEN (CallByValueReduce 0 THENA Auto)⋅) }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. m < n
⊢ radd-list(map(λk.x[k];[n, m + 1))) = r0

2
1. n : ℤ
2. m : ℤ
3. ¬m < n
4. x : {n..m + 1-} ⟶ ℝ
5. m = n ∈ ℤ
⊢ radd-list(map(λk.x[k];[n, m + 1))) = x[n]

3
1. n : ℤ
2. m : ℤ
3. m ≠ n
4. ¬m < n
5. x : {n..m + 1-} ⟶ ℝ
⊢ radd-list(map(λk.x[k];[n, m + 1))) = (radd-list(map(λk.x[k];[n, (m - 1) + 1))) + x[m])

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
    (\mSigma{}\{x[k]  |  n\mleq{}k\mleq{}m\}  =  if  m  <z  n  then  r0  if  (m  =\msubz{}  n)  then  x[n]  else  \mSigma{}\{x[k]  |  n\mleq{}k\mleq{}m  -  1\}  +  x[m]  fi  )


By

---

Latex:
(Auto
  THEN  Unfold  `rsum`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Repeat  (AutoSplit)
  THEN  (CallByValueReduce  0  THENA  Auto)\mcdot{})

---

Home Index