---

Step * 1 of Lemma radd-list-cons


1. L : ℝ List
2. x : ℝ
⊢ bdd-diff(radd-list([x / L]);λn.((x n) + (radd-list(L) n) + 0))
BY
{ (RW (HigherC (UnfoldTopC `radd-list`)) 0
   THEN (CallByValueReduceOnTypes [⌜ℝ List⌝] 0⋅ THENA Auto)⋅
   THEN Reduce 0
   THEN (CallByValueReduce 0⋅ THENA Auto)⋅
   THEN AutoSplit
   THEN Auto'
   THEN ((Auto THEN (RWW "accelerate-bdd-diff" 0 THENA Auto)) THEN AutoSplit)⋅) }

1
1. L : ℝ List
2. ||L|| + 1 ≠ 0
3. x : ℝ
4. ||L|| = 0 ∈ ℤ
⊢ bdd-diff(reg-seq-list-add([x / L]);λn.((x n) + (r0 n) + 0))

2
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))

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}  List
2.  x  :  \mBbbR{}
\mvdash{}  bdd-diff(radd-list([x  /  L]);\mlambda{}n.((x  n)  +  (radd-list(L)  n)  +  0))


By

---

Latex:
(RW  (HigherC  (UnfoldTopC  `radd-list`))  0
  THEN  (CallByValueReduceOnTypes  [\mkleeneopen{}\mBbbR{}  List\mkleeneclose{}]  0\mcdot{}  THENA  Auto)\mcdot{}
  THEN  Reduce  0
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)\mcdot{}
  THEN  AutoSplit
  THEN  Auto'
  THEN  ((Auto  THEN  (RWW  "accelerate-bdd-diff"  0  THENA  Auto))  THEN  AutoSplit)\mcdot{})

---

Home Index