|
deriv_sincos_ax[ T : TYPE FROM real ] : THEORY
BEGIN
ASSUMING
IMPORTING analysis@deriv_domain
connected_domain: ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
AUTO_REWRITE+ connected_domain
AUTO_REWRITE+ not_one_element
IMPORTING trig@trig_basic, analysis@derivatives
a,b,t: VAR T
k,alpha: VAR real
sin_continuous: AXIOM
continuous?[T](LAMBDA (x: T): k * sin(alpha * x))
cos_continuous: AXIOM
continuous?[T](LAMBDA (x: T): k * cos(alpha * x))
sin_derivable: AXIOM
derivable?[T](LAMBDA (x: T): k * sin(alpha * x))
cos_derivable: AXIOM
derivable?[T](LAMBDA (x: T): k * cos(alpha * x))
deriv_sin: AXIOM alpha /= 0 IMPLIES
deriv[T](LAMBDA (x:T): k*sin(alpha*x)) =
(LAMBDA (t: T): k*alpha*cos(alpha*t))
deriv_cos: AXIOM alpha /= 0 IMPLIES
deriv[T](LAMBDA (x:T): k*cos(alpha*x)) =
(LAMBDA (t: T): -k*alpha*sin(alpha*t))
END deriv_sincos_ax
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
