---

Step * 1 1 of Lemma addrcos_wf2


1. x : ℝ
2. n : ℕ+
⊢ |(addrcos(x) n) - (x + rcos(x)) n| ≤ 4
BY
{ (RepUR ``addrcos radd reg-seq-list-add`` 0
   THEN RepeatFor 3 (RecUnfold `cbv_list_accum` 0)
   THEN Reduce 0
   THEN RepUR ``rcos approx-arg accelerate`` 0
   THEN RepeatFor 6 ((CallByValueReduce 0 THENA Auto))
   THEN (Subst' 4 * 4 * n ~ 16 * n 0 THENA Auto)
   THEN (GenConcl ⌜(16 * n) = m ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(x m) = xm ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(cosine((r(xm))/2 * m) m) = z ∈ ℤ⌝⋅ THENA 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 ∈ ℤ
⊢ |((((m * z) ÷ 4 * m) + (xm ÷ 4)) ÷ 4) - ((0 + (x (4 * n))) + (z ÷ 4)) ÷ 4| ≤ 4

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  |(addrcos(x)  n)  -  (x  +  rcos(x))  n|  \mleq{}  4


By

---

Latex:
(RepUR  ``addrcos  radd  reg-seq-list-add``  0
  THEN  RepeatFor  3  (RecUnfold  `cbv\_list\_accum`  0)
  THEN  Reduce  0
  THEN  RepUR  ``rcos  approx-arg  accelerate``  0
  THEN  RepeatFor  6  ((CallByValueReduce  0  THENA  Auto))
  THEN  (Subst'  4  *  4  *  n  \msim{}  16  *  n  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(16  *  n)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(x  m)  =  xm\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(cosine((r(xm))/2  *  m)  m)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index