---

Step * 1 1 1 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
7. ∀m,x:ℤ.  ((2 * k) * m * (x ÷ 2 * k) ~ (m * x) - m * (x rem 2 * k))
8. r1 : {r:ℤ| |r| < |2 * k|} 
9. (f ((2 * k) * n) rem 2 * k) = r1 ∈ {r:ℤ| |r| < |2 * k|} 
10. r2 : {r:ℤ| |r| < |2 * k|} 
11. (f ((2 * k) * m) rem 2 * k) = r2 ∈ {r:ℤ| |r| < |2 * k|} 
12. |(m * (f ((2 * k) * n))) - m * r1 - (n * (f ((2 * k) * m))) - n * r2| ≤ (|(m * (f ((2 * k) * n))) - n
                                                                             * (f ((2 * k) * m))|
    + |-(m * r1)|
    + |n * r2|)
⊢ (|(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| + |-(m * r1)| + |n * r2|) ≤ (|2 * k| * 2 * (n + m))
BY
{ ((Assert (|-(m * r1)| + |n * r2|) ≤ (|2 * k| * (n + m)) BY
          ((RWO "absval_sym<" 0 THENA Auto)
           THEN (RWO "absval_mul" 0 THENA Auto)
           THEN (Assert |r1| ≤ |2 * k| BY
                       (DVar `r1' THEN Unhide THEN Auto))
           THEN (RWO "-1" 0 THENA Auto)
           THEN (Assert |r2| ≤ |2 * k| BY
                       (DVar `r2' THEN Unhide THEN Auto))
           THEN (RWO "-1" 0 THENA Auto)
           THEN RWO "absval_pos" 0
           THEN Auto))
   THEN RWO "-1" 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))
8. r1 : {r:ℤ| |r| < |2 * k|} 
9. (f ((2 * k) * n) rem 2 * k) = r1 ∈ {r:ℤ| |r| < |2 * k|} 
10. r2 : {r:ℤ| |r| < |2 * k|} 
11. (f ((2 * k) * m) rem 2 * k) = r2 ∈ {r:ℤ| |r| < |2 * k|} 
12. |(m * (f ((2 * k) * n))) - m * r1 - (n * (f ((2 * k) * m))) - n * r2| ≤ (|(m * (f ((2 * k) * n))) - n
                                                                             * (f ((2 * k) * m))|
    + |-(m * r1)|
    + |n * r2|)
13. (|-(m * r1)| + |n * r2|) ≤ (|2 * k| * (n + m))
⊢ (|(m * (f ((2 * k) * n))) - n * (f ((2 * k) * m))| + (|2 * k| * (n + m))) ≤ (|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
7.  \mforall{}m,x:\mBbbZ{}.    ((2  *  k)  *  m  *  (x  \mdiv{}  2  *  k)  \msim{}  (m  *  x)  -  m  *  (x  rem  2  *  k))
8.  r1  :  \{r:\mBbbZ{}|  |r|  <  |2  *  k|\} 
9.  (f  ((2  *  k)  *  n)  rem  2  *  k)  =  r1
10.  r2  :  \{r:\mBbbZ{}|  |r|  <  |2  *  k|\} 
11.  (f  ((2  *  k)  *  m)  rem  2  *  k)  =  r2
12.  |(m  *  (f  ((2  *  k)  *  n)))  -  m  *  r1  -  (n  *  (f  ((2  *  k)  *  m)))  -  n  *  r2| 
        \mleq{}  (|(m  *  (f  ((2  *  k)  *  n)))  -  n  *  (f  ((2  *  k)  *  m))|  +  |-(m  *  r1)|  +  |n  *  r2|)
\mvdash{}  (|(m  *  (f  ((2  *  k)  *  n)))  -  n  *  (f  ((2  *  k)  *  m))|  +  |-(m  *  r1)|  +  |n  *  r2|)  \mleq{}  (|2  *  k|
    *  2
    *  (n  +  m))


By

---

Latex:
((Assert  (|-(m  *  r1)|  +  |n  *  r2|)  \mleq{}  (|2  *  k|  *  (n  +  m))  BY
                ((RWO  "absval\_sym<"  0  THENA  Auto)
                  THEN  (RWO  "absval\_mul"  0  THENA  Auto)
                  THEN  (Assert  |r1|  \mleq{}  |2  *  k|  BY
                                          (DVar  `r1'  THEN  Unhide  THEN  Auto))
                  THEN  (RWO  "-1"  0  THENA  Auto)
                  THEN  (Assert  |r2|  \mleq{}  |2  *  k|  BY
                                          (DVar  `r2'  THEN  Unhide  THEN  Auto))
                  THEN  (RWO  "-1"  0  THENA  Auto)
                  THEN  RWO  "absval\_pos"  0
                  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index