| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 631 B |
|
Quelle trig_props.pvs Sprache: PVS |
|||||||||
|
trig_props: THEORY
BEGIN % analysis: LIBRARY "../analysis" IMPORTING power_series_deriv[real], trig_fun, analysis@derivative_props, analysis@deriv_domain n: VAR nat x: VAR real sin_derivable: LEMMA derivable?(sin); deriv_sin : THEOREM deriv(sin)(x) = cos(x) cos_derivable: LEMMA derivable?(cos); deriv_cos : THEOREM deriv(cos)(x) = -sin(x) sin2_cos2_derivable: LEMMA derivable?(sin*sin+cos*cos) sin2_cos2 : THEOREM sin*sin + cos*cos = const_fun(1) sin_cos_one : THEOREM sin(x)*sin(x) + cos(x)*cos(x) = 1 sin_lt_1 : LEMMA abs(sin(x)) <= 1 END trig_props ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28