---

Step * 2 1 of Lemma rsum_unroll


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]
BY
{ (RWO "radd-list-cons" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO  "radd-list-cons"  0  THEN  Auto)

---

Home Index