---

Step * 1 of Lemma accelerate-bdd-diff


1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
⊢ |((2 * k) * (accelerate(k;f) n)) - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 2))
BY
{ (RepUR ``accelerate`` 0
   THEN RepeatFor 2 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0))
   THEN (RWO "div_rem_sum2" 0 THENA Auto)) }

1
1. k : ℕ+@i
2. f : {f:ℕ+ ⟶ ℤ| k-regular-seq(f)} 
3. n : ℕ+@i
⊢ |(f ((2 * k) * n)) - f ((2 * k) * n) rem 2 * k - (2 * k) * (f n)| ≤ ((2 * k) * ((2 * k) + 2))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}@i
2.  f  :  \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  k-regular-seq(f)\} 
3.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  |((2  *  k)  *  (accelerate(k;f)  n))  -  (2  *  k)  *  (f  n)|  \mleq{}  ((2  *  k)  *  ((2  *  k)  +  2))


By

---

Latex:
(RepUR  ``accelerate``  0
  THEN  RepeatFor  2  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))
  THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto))

---

Home Index