---

Step * 2 of Lemma r-list-sum_functionality


1. u : ℝ
2. v : ℝ List
3. ∀[L2:ℝ List]. r-list-sum(v) = r-list-sum(L2) supposing (||v|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] = L2[i]))
4. u1 : ℝ
5. v1 : ℝ List
6. r-list-sum([u / v]) = r-list-sum(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] = v1[i]))
7. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
8. ∀i:ℕ||v|| + 1. ([u / v][i] = [u1 / v1][i])
9. 0 ≤ ||v||
⊢ u = u1
BY
{ ((D -2 With ⌜0⌝  THENA Auto) THEN Reduce -1 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  \mforall{}[L2:\mBbbR{}  List]
          r-list-sum(v)  =  r-list-sum(L2)  supposing  (||v||  =  ||L2||)  \mwedge{}  (\mforall{}i:\mBbbN{}||v||.  (v[i]  =  L2[i]))
4.  u1  :  \mBbbR{}
5.  v1  :  \mBbbR{}  List
6.  r-list-sum([u  /  v])  =  r-list-sum(v1) 
      supposing  (||[u  /  v]||  =  ||v1||)  \mwedge{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  ([u  /  v][i]  =  v1[i]))
7.  (||v||  +  1)  =  (||v1||  +  1)
8.  \mforall{}i:\mBbbN{}||v||  +  1.  ([u  /  v][i]  =  [u1  /  v1][i])
9.  0  \mleq{}  ||v||
\mvdash{}  u  =  u1


By

---

Latex:
((D  -2  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1  THEN  Auto)

---

Home Index