---

Step * 1 2 1 1 1 of Lemma radd-list-cons


1. L : ℝ List
2. ||L|| ≠ 0
3. ||L|| + 1 ≠ 0
4. x : ℝ
5. bdd-diff(λn.((0 + (x n)) + accelerate(||L||;reg-seq-list-add(L))[n]);λn.((0 + (x n)) + reg-seq-list-add(L)[n]))
6. n : Base
⊢ (x n) + (accelerate(||L||;reg-seq-list-add(L)) n) + 0 ~ (0 + (x n)) + (accelerate(||L||;reg-seq-list-add(L)) n)
BY
{ (RW (AddrC [2;1] (LemmaC `add-commutes`)) 0 THENA Auto) }

1
1. L : ℝ List
2. ||L|| ≠ 0
3. ||L|| + 1 ≠ 0
4. x : ℝ
5. bdd-diff(λn.((0 + (x n)) + accelerate(||L||;reg-seq-list-add(L))[n]);λn.((0 + (x n)) + reg-seq-list-add(L)[n]))
6. n : Base
⊢ (x n) + (accelerate(||L||;reg-seq-list-add(L)) n) + 0 ~ ((x n) + 0) + (accelerate(||L||;reg-seq-list-add(L)) n)

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}  List
2.  ||L||  \mneq{}  0
3.  ||L||  +  1  \mneq{}  0
4.  x  :  \mBbbR{}
5.  bdd-diff(\mlambda{}n.((0  +  (x  n))  +  accelerate(||L||;reg-seq-list-add(L))[n]);
                        \mlambda{}n.((0  +  (x  n))  +  reg-seq-list-add(L)[n]))
6.  n  :  Base
\mvdash{}  (x  n)  +  (accelerate(||L||;reg-seq-list-add(L))  n)  +  0  \msim{}  (0  +  (x  n))
+  (accelerate(||L||;reg-seq-list-add(L))  n)


By

---

Latex:
(RW  (AddrC  [2;1]  (LemmaC  `add-commutes`))  0  THENA  Auto)

---

Home Index