---

Step * 1 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 + (accelerate(2;x) k)) ÷ 4) - ((x k) + A) ÷ 4| ≤ 4
BY
{ (Assert 2-regular-seq(x) BY
         (DVar `x'
          THEN Unhide
          THEN Auto
          THEN RepeatFor 2 (ParallelOp 2)
          THEN ParallelLast'
          THEN RWO  "-1" 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 ∈ ℕ+
13. 2-regular-seq(x)
⊢ |((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  +  (accelerate(2;x)  k))  \mdiv{}  4)  -  ((x  k)  +  A)  \mdiv{}  4|  \mleq{}  4


By

---

Latex:
(Assert  2-regular-seq(x)  BY
              (DVar  `x'
                THEN  Unhide
                THEN  Auto
                THEN  RepeatFor  2  (ParallelOp  2)
                THEN  ParallelLast'
                THEN  RWO    "-1"  0
                THEN  Auto))

---

Home Index