---

Step * of Lemma r-list-sum_functionality

∀[L1,L2:ℝ List].  r-list-sum(L1) = r-list-sum(L2) supposing (||L1|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||L1||. (L1[i] = L2[i]))
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Reduce 0
   THEN Auto
   THEN (Assert 0 ≤ ||v|| BY
               Auto)
   THEN Auto
   THEN Unfold `r-list-sum` 0
   THEN Reduce 0
   THEN Fold `r-list-sum` 0
   THEN BLemma `radd_functionality`
   THEN Auto) }

1
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||
⊢ r-list-sum(v) = r-list-sum(v1)

2
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

---

Latex:

---

Latex:
\mforall{}[L1,L2:\mBbbR{}  List].
    r-list-sum(L1)  =  r-list-sum(L2)  supposing  (||L1||  =  ||L2||)  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (L1[i]  =  L2[i]))


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Reduce  0
  THEN  Auto
  THEN  (Assert  0  \mleq{}  ||v||  BY
                          Auto)
  THEN  Auto
  THEN  Unfold  `r-list-sum`  0
  THEN  Reduce  0
  THEN  Fold  `r-list-sum`  0
  THEN  BLemma  `radd\_functionality`
  THEN  Auto)

---

Home Index