| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle tan_approx.pvs Sprache: PVS |
|||||||||
|
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.4 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28