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