Quelle  trig_full.pvs   Sprache: PVS

trig_full: THEORY
%------------------------------------------------------------------------
%
% A Theory of Trigonometry
%
%       by Cesar Munoz
%          Victor Carreno
%          Ricky Butler
%          Gilles Dowek
%          Alfons Geser
%          Ben Di Vito
%          David Lester
% 
%------------------------------------------------------------------------

BEGIN
   IMPORTING trig,

             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,    % Approximations for tangent
             atan_approx,   % Approximations for atan 
             law_cosines,   % law of cosines
             trig_degree,   % conversions to degrees
             trig_inverses, % inverse functions
             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

% ---------------------- Foundational Development -----------------------

             sincos,        % continuity and differentiability of sin, cos
            
             sincos_phase,          % sin and cos from infinite series
             sincos,                % continuity, differentiality, and bounds
             sincos_quad,           % basic properties of sin cos
             tan_quad,              % definiton of tan from atan
             deriv_sincos

END trig_full