---

Step * 1 2 1 2 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]))
⊢ bdd-diff(reg-seq-list-add([x / L]);λn.((0 + (x n)) + accelerate(||L||;reg-seq-list-add(L))[n]))
BY
{ ((RWO "-1" 0 THENA Auto) THEN Thin (-1) THEN (BLemma `bdd-diff_weakening` THEN Auto)⋅) }

1
1. L : ℝ List
2. ||L|| ≠ 0
3. ||L|| + 1 ≠ 0
4. x : ℝ
⊢ reg-seq-list-add([x / L]) = (λn.((0 + (x n)) + 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]))
\mvdash{}  bdd-diff(reg-seq-list-add([x  /  L]);\mlambda{}n.((0  +  (x  n))  +  accelerate(||L||;reg-seq-list-add(L))[n]))


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)  THEN  Thin  (-1)  THEN  (BLemma  `bdd-diff\_weakening`  THEN  Auto)\mcdot{})

---

Home Index