---

Step * 1 of Lemma radd-list_functionality


1. L1 : ℝ List
2. L2 : ℝ List
3. ||L1|| = ||L2|| ∈ ℤ
4. ∀i:ℕ||L1||. (L1[i] = L2[i])
⊢ bdd-diff(λn.l_sum(map(λx.(x n);L1));λn.l_sum(map(λx.(x n);L2)))
BY
{ (RepeatFor 3 (MoveToConcl (-1)) THEN ListInd 1 THEN InductionOnList THEN Reduce 0 THEN Auto') }

1
1. 0 = 0 ∈ ℤ
2. ∀i:ℕ0. (⊥ = ⊥)
⊢ bdd-diff(λn.0;λn.0)

2
1. u : ℝ
2. v : ℝ List
3. ∀L2:ℝ List
     ((||v|| = ||L2|| ∈ ℤ)
     ⇒ (∀i:ℕ||v||. (v[i] = L2[i]))
     ⇒ bdd-diff(λn.l_sum(map(λx.(x n);v));λn.l_sum(map(λx.(x n);L2))))
4. u1 : ℝ
5. v1 : ℝ List
6. (||[u / v]|| = ||v1|| ∈ ℤ)
⇒ (∀i:ℕ||[u / v]||. ([u / v][i] = v1[i]))
⇒ bdd-diff(λn.l_sum(map(λx.(x n);[u / v]));λn.l_sum(map(λx.(x n);v1)))
7. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
8. ∀i:ℕ||v|| + 1. ([u / v][i] = [u1 / v1][i])
⊢ bdd-diff(λn.((u n) + l_sum(map(λx.(x n);v)));λn.((u1 n) + l_sum(map(λx.(x n);v1))))

---

Latex:

---

Latex:

1.  L1  :  \mBbbR{}  List
2.  L2  :  \mBbbR{}  List
3.  ||L1||  =  ||L2||
4.  \mforall{}i:\mBbbN{}||L1||.  (L1[i]  =  L2[i])
\mvdash{}  bdd-diff(\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);L1));\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);L2)))


By

---

Latex:
(RepeatFor  3  (MoveToConcl  (-1))  THEN  ListInd  1  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto')

---

Home Index