---

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