		Search-engine friendly clone of the ACL2 documentation.

Sin-cos

Fast-compute-cos

This function returns the numerator and denominator of a rational approximation to cos(x) (in radians) by itr iterations of fast-compute-series.

Definitions and Theorems

Function: fast-compute-cos

(defun fast-compute-cos (x itr)
  (declare (xargs :guard (and (rationalp x)
                              (integerp itr)
                              (>= itr 0))))
  (fast-compute-series (* (numerator x) (numerator x))
                       (* (denominator x) (denominator x))
                       1 1 1 0 nil itr))