---

Step * 1 2 2 1 of Lemma radd-list_functionality


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])
9. i : ℕ||v||
⊢ v[i] = v1[i]
BY
{ xxx(InstHyp [⌜i + 1⌝] (-2)⋅ THEN Auto)xxx }

1
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])
9. i : ℕ||v||
10. [u / v][i + 1] = [u1 / v1][i + 1]
⊢ v[i] = v1[i]

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  \mforall{}L2:\mBbbR{}  List
          ((||v||  =  ||L2||)
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||v||.  (v[i]  =  L2[i]))
          {}\mRightarrow{}  bdd-diff(\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);v));\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);L2))))
4.  u1  :  \mBbbR{}
5.  v1  :  \mBbbR{}  List
6.  (||[u  /  v]||  =  ||v1||)
{}\mRightarrow{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  ([u  /  v][i]  =  v1[i]))
{}\mRightarrow{}  bdd-diff(\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);[u  /  v]));\mlambda{}n.l\_sum(map(\mlambda{}x.(x  n);v1)))
7.  (||v||  +  1)  =  (||v1||  +  1)
8.  \mforall{}i:\mBbbN{}||v||  +  1.  ([u  /  v][i]  =  [u1  /  v1][i])
9.  i  :  \mBbbN{}||v||
\mvdash{}  v[i]  =  v1[i]


By

---

Latex:
xxx(InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)xxx

---

Home Index