| products/sources/formale sprachen/PVS/analysis_ax/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: continuous_lambda.prf Sprache: PVSOriginal von: PVS© |
|
||||||
|
continuous_lambda [ T : TYPE FROM real ] : THEORY
BEGIN IMPORTING continuous_functions[T], reals@min_max, reals@sq f,g : VAR continuous_fun pos_continuous?(f):bool = FORALL (x:T) : f(x) > 0 pos_continuous_fun : TYPE = (pos_continuous?) nzf : VAR nz_continuous_fun pf : VAR pos_continuous_fun x : VAR T k : VAR real nzk : VAR nzreal n : VAR nat id_cont : LEMMA continuous?(LAMBDA(x):x) const_cont: LEMMA continuous?(LAMBDA(x):k) add_cont : LEMMA continuous?(LAMBDA(x):f(x)+g(x)) sub_cont : LEMMA continuous?(LAMBDA(x):f(x)-g(x)) neg_cont : LEMMA continuous?(LAMBDA(x):-f(x)) mult_cont : LEMMA continuous?(LAMBDA(x):f(x)*g(x)) div_cont : LEMMA continuous?(LAMBDA(x):f(x)/nzf(x)) scal_mult_cont : LEMMA continuous?(LAMBDA(x):k*f(x)) scal_div1_cont : LEMMA continuous?(LAMBDA(x):f(x)/nzk) scal_div2_cont : LEMMA continuous?(LAMBDA(x):k/nzf(x)) pow_cont : LEMMA continuous?(LAMBDA(x):f(x)^n) sq_cont : LEMMA continuous?(LAMBDA (x):sq(f(x))) IMPORTING sqrt_derivative, composition_continuous sqrt_cont : LEMMA continuous?(LAMBDA(x):sqrt(pf(x))) abs_cont : LEMMA continuous?(LAMBDA (x):abs(f(x))) max_cont : LEMMA continuous?(LAMBDA (x):max(f(x),g(x))) min_cont : LEMMA continuous?(LAMBDA (x):min(f(x),g(x))) END continuous_lambda ¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
