---

Step * 1 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])
⊢ bdd-diff(λ2n.u n;λ2n.u1 n)
BY
{ xxx((InstHyp [⌜0⌝] (-1)⋅ THENA Auto) THEN Reduce (-1))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. u = u1
⊢ bdd-diff(λ2n.u n;λ2n.u1 n)

---

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])
\mvdash{}  bdd-diff(\mlambda{}\msubtwo{}n.u  n;\mlambda{}\msubtwo{}n.u1  n)


By

---

Latex:
xxx((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))xxx

---

Home Index