atan_values.pvs   Interaktion und
PortierbarkeitPVS

atan_values: THEORY
%------------------------------------------------------------------------------
%
%  Rick Butler    NASA Langley
% 
%------------------------------------------------------------------------------
BEGIN

  IMPORTING atan, trig_values, trig_inverses

  atan0        : LEMMA atan(0) = 0                   %% atan_0 already used

  atan1        : LEMMA atan(1) = pi/4                %% atan_1 already used

  atan_1sqrt3  : LEMMA atan(1/sqrt(3)) = pi/6

  atan_sqrt3   : LEMMA atan(sqrt(3))   = pi/3

  atan_m1sqrt3 : LEMMA atan(-1/sqrt(3)) = -pi/6

  atan_msqrt3  : LEMMA atan(-sqrt(3))   = -pi/3

  
  x: VAR real
  atan_gt_0    : LEMMA atan(x) > 0 IFF x > 0


END atan_values