---

Step * 1 2 of Lemma radd-list-cons


1. L : ℝ List
2. ||L|| ≠ 0
3. ||L|| + 1 ≠ 0
4. x : ℝ
⊢ bdd-diff(reg-seq-list-add([x / L]);λn.((x n) + (accelerate(||L||;reg-seq-list-add(L)) n) + 0))
BY
{ (InstLemma `bdd-diff-add` [⌜λ2n.0 + (x n)⌝;⌜λ2n.0 + (x n)⌝;⌜accelerate(||L||;reg-seq-list-add(L))⌝;
   ⌜reg-seq-list-add(L)⌝]⋅
   THENA (Auto THEN BLemma `bdd-diff_weakening` THEN 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]))
⊢ bdd-diff(reg-seq-list-add([x / L]);λn.((x n) + (accelerate(||L||;reg-seq-list-add(L)) n) + 0))

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `bdd-diff-add`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.0  +  (x  n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.0  +  (x  n)\mkleeneclose{};\mkleeneopen{}accelerate(||L||;reg-seq-list-add(L))\mkleeneclose{};
  \mkleeneopen{}reg-seq-list-add(L)\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  BLemma  `bdd-diff\_weakening`  THEN  Auto)
  )

---

Home Index