---

Step * 1 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
⊢ |(2 * k) * ((m * ((f ((2 * k) * n)) ÷ 2 * k)) - n * ((f ((2 * k) * m)) ÷ 2 * k))| ≤ (|2 * k| * 2 * (n + m))
BY
{ (Assert ∀m,x:ℤ.  ((2 * k) * m * (x ÷ 2 * k) ~ (m * x) - m * (x rem 2 * k)) BY
         (Auto
          THEN (Subst' (2 * k) * m1 * (x ÷ 2 * k) ~ m1 * (2 * k) * (x ÷ 2 * k) 0 THEN Auto)
          THEN RWO "div_rem_sum2" 0
          THEN Auto)) }

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
7. ∀m,x:ℤ.  ((2 * k) * m * (x ÷ 2 * k) ~ (m * x) - m * (x rem 2 * k))
⊢ |(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{}  |(2  *  k)  *  ((m  *  ((f  ((2  *  k)  *  n))  \mdiv{}  2  *  k))  -  n  *  ((f  ((2  *  k)  *  m))  \mdiv{}  2  *  k))|  \mleq{}  (|2  *  k|
    *  2
    *  (n  +  m))


By

---

Latex:
(Assert  \mforall{}m,x:\mBbbZ{}.    ((2  *  k)  *  m  *  (x  \mdiv{}  2  *  k)  \msim{}  (m  *  x)  -  m  *  (x  rem  2  *  k))  BY
              (Auto
                THEN  (Subst'  (2  *  k)  *  m1  *  (x  \mdiv{}  2  *  k)  \msim{}  m1  *  (2  *  k)  *  (x  \mdiv{}  2  *  k)  0  THEN  Auto)
                THEN  RWO  "div\_rem\_sum2"  0
                THEN  Auto))

---

Home Index