| products/sources/formale sprachen/PVS/trig/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Testjava.java Sprache: PVSUntersuchung PVS© |
|
||||||
|
acos: THEORY
BEGIN IMPORTING asin, reals@abs_lems nnreal_le_pi: NONEMPTY_TYPE = {x:nnreal | x <= pi} CONTAINING 0 x: VAR real_abs_le1 xne: VAR real_abs_lt1 nnx,nny: VAR {x:nnreal | x <= 1} acos(x:real_abs_le1):nnreal_le_pi = pi/2 - asin(x) acos_neg: LEMMA acos(-x) = pi-acos(x) acos_0: LEMMA acos(0) = pi/2 acos_sqrt_half: LEMMA acos(sqrt(1/2)) = pi/4 acos_1: LEMMA acos(1) = 0 acos_minus1: LEMMA acos(-1) = pi acos_minus_sqrt_half: LEMMA acos(-sqrt(1/2)) = 3*pi/4 acos_strict_decreasing: LEMMA strict_decreasing?(acos) acos_bij: LEMMA bijective?[real_abs_le1,nnreal_le_pi](acos) acos_sum: LEMMA % 4.4.32 acos(nnx)+acos(nny) = acos(nnx*nny-(sqrt(1-sq(nny)))*(sqrt(1-sq(nnx)))) % acos_derivable: LEMMA % derivable[real_abs_lt1]((LAMBDA (x:real_abs_lt1):acos(x)),xne) % acos_derivable2: LEMMA % derivable[real_abs_lt1](LAMBDA (x:real_abs_lt1): acos(x)) % deriv_acos_fun: LEMMA deriv[real_abs_lt1](LAMBDA (x:real_abs_lt1): acos(x)) % = (LAMBDA (x:real_abs_lt1): -deriv(LAMBDA (x: real_abs_lt1): asin(x))(x)) END acos ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
