Step
*
1
of Lemma
rsum-single
1. n : ℤ
2. x : {i:ℤ| i = n ∈ ℤ} ⟶ ℝ
⊢ let xs ⟵ map(λi.x[i];[n, n + 1)) in radd-list(xs) = x[n]
BY
{ ((RWO "from-upto-single" 0 THENA Auto) THEN Reduce 0 THEN (CallByValueReduce 0 THENA Auto))⋅ }
1
1. n : ℤ
2. x : {i:ℤ| i = n ∈ ℤ} ⟶ ℝ
⊢ radd-list([x[n]]) = x[n]
Latex:
Latex:
1. n : \mBbbZ{}
2. x : \{i:\mBbbZ{}| i = n\} {}\mrightarrow{} \mBbbR{}
\mvdash{} let xs \mleftarrow{}{} map(\mlambda{}i.x[i];[n, n + 1)) in radd-list(xs) = x[n]
By
Latex:
((RWO "from-upto-single" 0 THENA Auto) THEN Reduce 0 THEN (CallByValueReduce 0 THENA Auto))\mcdot{}
Home
Index