Step
*
3
of Lemma
rsum_unroll
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])
BY
{ Subst ⌜[n, m + 1) ~ [n, (m - 1) + 1) @ [m]⌝ 0⋅ }
1
.....equality.....
1. n : ℤ
2. m : ℤ
3. m ≠ n
4. ¬m < n
5. x : {n..m + 1-} ⟶ ℝ
⊢ [n, m + 1) ~ [n, (m - 1) + 1) @ [m]
2
1. n : ℤ
2. m : ℤ
3. m ≠ n
4. ¬m < n
5. x : {n..m + 1-} ⟶ ℝ
⊢ radd-list(map(λk.x[k];[n, (m - 1) + 1) @ [m])) = (radd-list(map(λk.x[k];[n, (m - 1) + 1))) + x[m])
Latex:
Latex:
1. n : \mBbbZ{}
2. m : \mBbbZ{}
3. m \mneq{} n
4. \mneg{}m < n
5. x : \{n..m + 1\msupminus{}\} {}\mrightarrow{} \mBbbR{}
\mvdash{} radd-list(map(\mlambda{}k.x[k];[n, m + 1))) = (radd-list(map(\mlambda{}k.x[k];[n, (m - 1) + 1))) + x[m])
By
Latex:
Subst \mkleeneopen{}[n, m + 1) \msim{} [n, (m - 1) + 1) @ [m]\mkleeneclose{} 0\mcdot{}
Home
Index