---

Step * 2 of Lemma rsum_unroll


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]
BY
{ ((RecUnfold `from-upto` 0 THEN AutoSplit)⋅
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RecUnfold `from-upto` 0
   THEN AutoSplit) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  \mneg{}m  <  n
4.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
5.  m  =  n
\mvdash{}  radd-list(map(\mlambda{}k.x[k];[n,  m  +  1)))  =  x[n]


By

---

Latex:
((RecUnfold  `from-upto`  0  THEN  AutoSplit)\mcdot{}
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RecUnfold  `from-upto`  0
  THEN  AutoSplit)

---

Home Index