---

Step * 1 of Lemma rcosine_wf


1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. p : ℝ
5. p = π/2
6. |x - n * p| ≤ r(2)
7. -(r(2)) ≤ (x - n * p)
8. (x - n * p) ≤ r(2)
⊢ if (n mod 4 =z 0) then cosine-medium(x - n * p)
if (n mod 4 =z 2) then -(cosine-medium(x - n * p))
if (n mod 4 =z 1) then -(sine-medium(x - n * p))
else sine-medium(x - n * p)
fi 
= rcos(x)
BY
{ (GenConclTerms  Auto [⌜sine-medium(x - n * p)⌝;⌜cosine-medium(x - n * p)⌝]⋅
   THEN Thin (-3)
   THEN Thin (-1)
   THEN D -2
   THEN D -1
   THEN (Unhide THENA Auto)
   THEN (RWO "5" (-3) THENA Auto)
   THEN (RWO "5" (-1) THENA Auto)
   THEN (RWO "5" (7) THENA Auto)
   THEN (RWO "5" (8) THENA Auto)
   THEN ThinVar `p'
   THEN (RWO "rsin-is-sine<" (-3) THENA Auto)
   THEN (RWO "rsin-reduce-half-pi" (-3) THENA Auto)
   THEN (RWO "rcos-is-cosine<" (-1) THENA Auto)
   THEN (RWO "rcos-reduce-half-pi" (-1) THENA Auto)) }

1
1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. -(r(2)) ≤ (x - n * π/2)
5. (x - n * π/2) ≤ r(2)
6. v : ℝ
7. v
= if (n mod 4 =z 0) then rsin(x)
  if (n mod 4 =z 2) then -(rsin(x))
  if (n mod 4 =z 1) then -(rcos(x))
  else rcos(x)
  fi 
8. v1 : ℝ
9. v1
= if (n mod 4 =z 0) then rcos(x)
  if (n mod 4 =z 2) then -(rcos(x))
  if (n mod 4 =z 1) then rsin(x)
  else -(rsin(x))
  fi 
⊢ if (n mod 4 =z 0) then v1 if (n mod 4 =z 2) then -(v1) if (n mod 4 =z 1) then -(v) else v fi  = rcos(x)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbZ{}
3.  |x  -  r(n)  *  \mpi{}/2|  \mleq{}  r(2)
4.  p  :  \mBbbR{}
5.  p  =  \mpi{}/2
6.  |x  -  n  *  p|  \mleq{}  r(2)
7.  -(r(2))  \mleq{}  (x  -  n  *  p)
8.  (x  -  n  *  p)  \mleq{}  r(2)
\mvdash{}  if  (n  mod  4  =\msubz{}  0)  then  cosine-medium(x  -  n  *  p)
if  (n  mod  4  =\msubz{}  2)  then  -(cosine-medium(x  -  n  *  p))
if  (n  mod  4  =\msubz{}  1)  then  -(sine-medium(x  -  n  *  p))
else  sine-medium(x  -  n  *  p)
fi 
=  rcos(x)


By

---

Latex:
(GenConclTerms    Auto  [\mkleeneopen{}sine-medium(x  -  n  *  p)\mkleeneclose{};\mkleeneopen{}cosine-medium(x  -  n  *  p)\mkleeneclose{}]\mcdot{}
  THEN  Thin  (-3)
  THEN  Thin  (-1)
  THEN  D  -2
  THEN  D  -1
  THEN  (Unhide  THENA  Auto)
  THEN  (RWO  "5"  (-3)  THENA  Auto)
  THEN  (RWO  "5"  (-1)  THENA  Auto)
  THEN  (RWO  "5"  (7)  THENA  Auto)
  THEN  (RWO  "5"  (8)  THENA  Auto)
  THEN  ThinVar  `p'
  THEN  (RWO  "rsin-is-sine<"  (-3)  THENA  Auto)
  THEN  (RWO  "rsin-reduce-half-pi"  (-3)  THENA  Auto)
  THEN  (RWO  "rcos-is-cosine<"  (-1)  THENA  Auto)
  THEN  (RWO  "rcos-reduce-half-pi"  (-1)  THENA  Auto))

---

Home Index