| products/sources/formale sprachen/PVS/structures/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: shift.pvs Sprache: Unknown
|
tan_approx : THEORY
%----------------------------------------------------------------------------- % tan_approx % ----------- % tangent approximations % Cesar Munoz (Feb 6 2004) % %----------------------------------------------------------------------------- BEGIN IMPORTING trig_approx n : VAR nat a,b : VAR real % Approximations tan tan_lb_ub(a:real,(n|cos_ub(a,n) /= 0)): real = sin_lb(a,n)/cos_ub(a,n) tan_ub_lb(a:real,(n|cos_lb(a,n) /= 0)): real = sin_ub(a,n)/cos_lb(a,n) tan_lb_lb(a:real,(n|cos_lb(a,n) /= 0)): real = sin_lb(a,n)/cos_lb(a,n) tan_ub_ub(a:real,(n|cos_ub(a,n) /= 0)): real = sin_ub(a,n)/cos_ub(a,n) tan_lb_ub_neg : LEMMA cos_ub(a,n) /= 0 IMPLIES tan_lb_ub(-a,n) = -tan_ub_ub(a,n) tan_ub_lb_neg : LEMMA cos_lb(a,n) /= 0 IMPLIES tan_ub_lb(-a,n) = -tan_lb_lb(a,n) tan_lb_lb_neg : LEMMA cos_lb(a,n) /= 0 IMPLIES tan_lb_lb(-a,n) = -tan_ub_lb(a,n) tan_ub_ub_neg : LEMMA cos_ub(a,n) /= 0 IMPLIES tan_ub_ub(-a,n) = -tan_lb_ub(a,n) tan_bounds_0_pi2 : LEMMA 0 <= a AND a < pi/2 AND cos_lb(a,n) > 0 IMPLIES tan_lb_ub(a,n) <= tan(a) AND tan(a) <= tan_ub_lb(a,n) tan_bounds_npi2_0 : LEMMA -pi/2 < a AND a <= 0 AND cos_lb(a,n) > 0 IMPLIES tan_lb_lb(a,n) <= tan(a) AND tan(a) <= tan_ub_ub(a,n) tan_bounds_pi2_pi : LEMMA pi/2 < a AND a <= pi AND cos_ub(a,n) < 0 IMPLIES tan_ub_ub(a,n) <= tan(a) AND tan(a) <= tan_lb_lb(a,n) tan_bounds_npi_npi2 : LEMMA -pi <= a AND a < -pi/2 AND cos_ub(a,n) < 0 IMPLIES tan_ub_lb(a,n) <= tan(a) AND tan(a) <= tan_lb_ub(a,n) END tan_approx [ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ] |