---

Step * 1 1 1 1 1 1 of Lemma addrcos_wf2


1. x : ℝ
2. n : ℕ+
3. m : ℤ
4. (16 * n) = m ∈ ℤ
5. xm : ℤ
6. (x m) = xm ∈ ℤ
7. z : ℤ
8. (cosine((r(xm))/2 * m) m) = z ∈ ℤ
9. A : ℤ
10. (z ÷ 4) = A ∈ ℤ
11. k : ℕ+
12. (4 * n) = k ∈ ℕ+
⊢ |((A + ((x (4 * k)) ÷ 4)) ÷ 4) - ((x k) + A) ÷ 4| ≤ 4
BY
{ (Subst' (x (4 * k)) ÷ 4 ~ accelerate(2;x) k 0 THENA (RepUR ``accelerate`` 0 THEN CallByValueReduce 0 THEN Auto)) }

1
1. x : ℝ
2. n : ℕ+
3. m : ℤ
4. (16 * n) = m ∈ ℤ
5. xm : ℤ
6. (x m) = xm ∈ ℤ
7. z : ℤ
8. (cosine((r(xm))/2 * m) m) = z ∈ ℤ
9. A : ℤ
10. (z ÷ 4) = A ∈ ℤ
11. k : ℕ+
12. (4 * n) = k ∈ ℕ+
⊢ |((A + (accelerate(2;x) k)) ÷ 4) - ((x k) + A) ÷ 4| ≤ 4

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  m  :  \mBbbZ{}
4.  (16  *  n)  =  m
5.  xm  :  \mBbbZ{}
6.  (x  m)  =  xm
7.  z  :  \mBbbZ{}
8.  (cosine((r(xm))/2  *  m)  m)  =  z
9.  A  :  \mBbbZ{}
10.  (z  \mdiv{}  4)  =  A
11.  k  :  \mBbbN{}\msupplus{}
12.  (4  *  n)  =  k
\mvdash{}  |((A  +  ((x  (4  *  k))  \mdiv{}  4))  \mdiv{}  4)  -  ((x  k)  +  A)  \mdiv{}  4|  \mleq{}  4


By

---

Latex:
(Subst'  (x  (4  *  k))  \mdiv{}  4  \msim{}  accelerate(2;x)  k  0
  THENA  (RepUR  ``accelerate``  0  THEN  CallByValueReduce  0  THEN  Auto)
  )

---

Home Index