---

Step * 1 of Lemma accelerate_wf

.....set predicate..... 
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. accelerate(k;f) ∈ ℕ+ ⟶ ℤ
4. k-regular-seq(f)
⊢ regular-seq(accelerate(k;f))
BY
{ (Unfold `regular-int-seq` -1 THEN D 0 THEN Auto THEN Reduce 0)⋅ }

1
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. accelerate(k;f) ∈ ℕ+ ⟶ ℤ
4. ∀n,m:ℕ+.  (|(m * (f n)) - n * (f m)| ≤ ((2 * k) * (n + m)))
5. n : ℕ+@i
6. m : ℕ+@i
⊢ |(m * (accelerate(k;f) n)) - n * (accelerate(k;f) m)| ≤ (2 * (n + m))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  k  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  accelerate(k;f)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  k-regular-seq(f)
\mvdash{}  regular-seq(accelerate(k;f))


By

---

Latex:
(Unfold  `regular-int-seq`  -1  THEN  D  0  THEN  Auto  THEN  Reduce  0)\mcdot{}

---

Home Index