| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Delphi/Agenda 1.1/ (Columbo Version 0.7©) Datei vom 4.1.2008 mit Größe 312 B |
|
trig_rew.pvs
Interaktion und |
|||||||||
|
trig_rew: THEORY
BEGIN %----------------------------------------------------------------------------- % % Experimental auto-rewrite-theory background trigonometry library % % Users should be able to issue % % (auto-rewrite_theory "trig_rew") % % at the beginning of a proof to automatically simplify formulas % %----------------------------------------------------------------------------- IMPORTING trig_basic a,b,c,d : VAR real nnc : VAR nonneg_real j,k,kk : VAR integer n: VAR nat % cos2 : LEMMA sq(cos(a)) = 1 - sq(sin(a)) tr_rew1 : LEMMA cos(0) = 1 tr_rew2 : LEMMA sin(0) = 0 tr_rew3 : LEMMA sin(pi/2) = 1 tr_rew4 : LEMMA cos(pi/2) = 0 tr_rew5 : LEMMA tan(0)=0 tr_rew6 : LEMMA sin(pi) = 0 tr_rew7 : LEMMA cos(pi) = -1 tr_rew8 : LEMMA tan(pi) = 0 tr_rew9 : LEMMA sin(3*pi/2) = -1 tr_rew10 : LEMMA cos(3*pi/2) = 0 tr_rew11 : LEMMA sin(2*pi) = 0 tr_rew12 : LEMMA cos(2*pi) = 1 tr_rew13 : LEMMA tan(2*pi) = 0 tr_rew14 : LEMMA sin(pi/2 - a) = cos(a) tr_rew15 : LEMMA cos(pi/2 - a) = sin(a) tr_rew16 : LEMMA sin(k*pi) = 0 tr_rew17 : LEMMA cos(2*k*pi) = 1 % tr_rew18 : LEMMA cos(k*pi) = (-1)^(k) % tr_rew19 : LEMMA sin(k*pi + pi/2) = (-1)^k tr_rew20 : LEMMA tan(k*pi) = 0 tr_rew22 : LEMMA sin(-a) = -sin(a) tr_rew23 : LEMMA cos(-a) = cos(a) tr_rew24 : LEMMA FORALL(a:(Tan?)): tan(-a) = -tan(a) END trig_rew ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28