| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle real_fun_ops.pvs Sprache: PVS |
|||||||||
|
real_fun_ops [ T : TYPE ] : THEORY
%------------------------------------------% % Operations on functions : [ T -> real] % %------------------------------------------% BEGIN f, f1, f2 : VAR [T -> real] f3 : VAR [T -> nzreal] a : VAR real x, y : VAR T const_fun(a) : [T -> real] = LAMBDA x : a ; +(f1, f2) : [T -> real] = LAMBDA x : f1(x) + f2(x); -(f1) : [T -> real] = LAMBDA x : -f1(x); *(f1, f2) : [T -> real] = LAMBDA x : f1(x) * f2(x); *(a, f1) : [T -> real] = LAMBDA x : a * f1(x); -(f1, f2) : [T -> real] = LAMBDA x : f1(x) - f2(x); /(f1, f3) : [T -> real] = LAMBDA x : f1(x) / f3(x); /(a, f3) : [T -> real] = LAMBDA x : a / f3(x); inv(f3) : [T -> real] = 1 / f3; abs(f1) : [T -> nonneg_real] = LAMBDA x : abs(f1(x)); n: VAR nat ^(f,n) : [T -> real] = (LAMBDA (t:T): f(t)^n) %------------------ % Rewrite rules %------------------ diff_function : LEMMA f1 - f2 = f1 + (- f2) div_function : LEMMA f1 / f3 = f1 * (1 /f3) scal_function : LEMMA a * f1 = const_fun(a) * f1 scaldiv_function : LEMMA a / f3 = const_fun(a) / f3 negneg_function : LEMMA - (- f1) = f1 END real_fun_ops ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28