Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Sprache: Unknown
|
% A couple of useful results to add to trig@trig_basic
% DRL
trig_aux: THEORY
BEGIN
IMPORTING trig@trig_basic
a,b: VAR real
i: VAR int
sin_cos_eq_0: LEMMA NOT (sin(a) = 0 AND cos(a) = 0)
eq_iff_periodic: LEMMA sin(a) = sin(b) AND cos(a) = cos(b) IFF
EXISTS i: a = b + 2*i*pi
END trig_aux
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
|
