## Top File of PVS trig Library

```
top: THEORY
%------------------------------------------------------------------------
%
% An Axiomatic Theory of Trigonometry (Demonstrated to be sound in trig_fnd
%                                      library)
%
%       by Cesar Munoz                     Langley ICASE Institute
%          Victor Carreno                  NASA Langley
%          Ricky Butler                    NASA Langley
%          Gilles Dowek                    INRIA, Domaine de Voluceau
%          Alfons Geser                    Langley ICASE Institute
%          Ben Di Vito                     NASA Langley
%
%      Version 1.0    3/27/01
%      Version 1.1    6/27/01              New lemmas added:
%                                          --------------------------------
%                                          tan_period, sin_k_pi , cos_2k_pi,
%                                          cos_k_pi  , sin_k_pi2, tan_k_pi,
%                                          sin_eq_1  , cos_eq_1 , sin_eq_sin,
%                                          cos_eq_cos, tan_eq_tan, sin_eq_pm1,
%                                          cos_eq_pm1, and prelude_aux lemmas
%
%      Version 1.2    6/28/01              Theory "trig_rew" added
%
%      Version 1.3    10/27/03             Corrected, foundational theory
%                                          (David Lester)
%
%      Version 1.31   11/29/03             Renamed PI to pi (Cesar A. Munoz)
%
%      Version 1.32   2/6/04               Theory "tan_approx" added (C. Munoz)
%
%      Version 1.33   5/23/04              atan2 added (D Lester)
%
%      Version 1.34   5/30/04              atan/asin/acos added (D Lester)
%
%      Version 1.4    4/15/05              approx made consistent with trig_fnd
%
% INDEX:
% ------
%
%
%     trig_basic:
%     -----------
%         - definition of pi with crude upper and lower bounds
%         - definition of sin, cos, and tan
%         - pythagorean properties: sq(sin(a)) + sq(cos(a)) = 1
%         - sum and difference of two angles
%         - double angle formulas
%         - negative properties, e.g. sin(-a)
%         - periodicity, e.g. sin(a) = sin(a + 2 * j * pi)
%         - co-function identities, e.g. sin(pi/2 - a) = cos(a)
%         - location of zeros of trig functions
%
%      trig_values                            Lemma names
%      -----------                   ------------------------------------
%         - trig functions at 0      : sin_0     , cos_0     , tan_0
%         - trig functions at pi/6   : sin_pi6   , cos_pi6   , tan_pi6
%         - trig functions at pi/4   : sin_pi4   , cos_pi4   , tan_pi4
%         - trig functions at pi/3   : sin_pi3   , cos_pi3   , tan_pi3
%         - trig functions at pi/2   : sin_pi2   , cos_pi2   , tan_pi2
%         - trig functions at pi     : sin_pi    , cos_pi    , tan_pi
%         - trig functions at 2*pi/3 : sin_2pi3  , cos_2pi3  , tan_2pi3
%         - trig functions at 3*pi/4 : sin_3pi4  , cos_3pi4  , tan_3pi4
%         - trig functions at 5*pi/4 : sin_5pi4  , cos_5pi4  , tan_5pi4
%
%      trig_ineq
%      ---------
%         - regions where functions are greater than 0
%         - regions where functions are less    than 0
%         - regions where functions are increasing
%         - regions where functions are decreasing
%
%      trig_extra
%      ----------
%         - reduction theorems
%         - sum and product identities
%         - half-angle identities and zeros
%         - triple angle formulas
%
%      trig_approx
%      -----------
%          - taylor series approximations to trig functions:
%               sin_approx(a,n): sum first n terms of taylor expansion of sin
%               cos_approx(a,n): sum first n terms of taylor expansion of cos
%
%      tan_approx
%      ----------
%          - taylor series approximations for tangent
%
%      law_cosines
%      -----------
%         - the law of cosines in a coordinate geometry formulation
%
%      trig_degree
%      -----------
%         - trig functions that take arguments in degrees: sind, cosd
%         - defines conversions toRad, toDeg
%
%      trig_inv
%      -------------
%         - provides interface to atan, asin, acos, atan2
%
%      -------------
%         - defines inverse trig functions: arcsin, arccos, and arctan
%
%      trig_rew
%      -------------
%         - Experimental auto-rewrite-theory background library
%
%
%------------------------------------------------------------------------

BEGIN
IMPORTING trig_doc,      % Some more documentation (Rationale)

trig,          % typical needs
trig_full,     % everything

% --------------------- The above import the following ------------------

trig_basic,    % basic properties
trig_values,   % values of functions for special arguments
trig_ineq,     % trig inequalities
trig_extra,    % sum and product, half-angle, reductions and zeros
trig_approx,   % taylor series approximations to trig functions:
tan_approx,    % approximatan2_propsations fprior tangent
law_cosines,   % law of cosines
trig_degree,   % conversions to degrees
trig_inverses, % interface to atan, asin, acos, atan2
trig_rew,      % auto-rewrites
asin,          % asin properties
acos,          % acos properties
atan,          % atan properties
atan_values,   % atan for specific values
atan2,         % two-argument arc tangent
atan2_props,   % additional properties of atan2 and values
jatan2,        % Java atan2

to2pi,         % normalization of radians to 2pi

sincos,        % continuity, derivablility of sin, cos
deriv_sincos,
integral_sincos,
integral_indef_sincos

END top

```
The tag identifies links that are outside the NASA domain