---

Step * 1 1 of Lemma accelerate_wf


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))
BY
{ ((Using [`n', ⌜|2 * k|⌝] (BLemma `mul_cancel_in_le`)⋅ THENA Auto)
   THEN (RWO "absval_mul<" 0 THENA Auto)
   THEN RepUR ``accelerate`` 0
   THEN RepeatFor 2 (((CallByValueReduceOnTypes [⌜ℤ⌝] 0⋅ THENA 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
⊢ |(2 * k) * ((m * ((f ((2 * k) * n)) ÷ 2 * k)) - n * ((f ((2 * k) * m)) ÷ 2 * k))| ≤ (|2 * k| * 2 * (n + m))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  accelerate(k;f)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
4.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (f  n))  -  n  *  (f  m)|  \mleq{}  ((2  *  k)  *  (n  +  m)))
5.  n  :  \mBbbN{}\msupplus{}@i
6.  m  :  \mBbbN{}\msupplus{}@i
\mvdash{}  |(m  *  (accelerate(k;f)  n))  -  n  *  (accelerate(k;f)  m)|  \mleq{}  (2  *  (n  +  m))


By

---

Latex:
((Using  [`n',  \mkleeneopen{}|2  *  k|\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_le`)\mcdot{}  THENA  Auto)
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto)
  THEN  RepUR  ``accelerate``  0
  THEN  RepeatFor  2  (((CallByValueReduceOnTypes  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{}]  0\mcdot{}  THENA  Auto)  THEN  Reduce  0)))

---

Home Index