| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1018 B |
|
Quelle vect_fun_ops_rv.pvs Sprache: PVS |
|||||||||
|
vect_fun_ops_rv [T: TYPE] : THEORY
%------------------------------------------% % Operations on functions : [ T -> Vect2] % %------------------------------------------% BEGIN IMPORTING vectors@vectors_2D f, f1, f2: VAR [T -> Vect2] x : VAR T a,b : VAR real r: VAR [T -> real] v: VAR Vect2 +(f1, f2) : MACRO [T -> Vect2] = LAMBDA x : f1(x) + f2(x); -(f1) : MACRO [T -> Vect2] = LAMBDA x : -f1(x); -(f1, f2) : MACRO [T -> Vect2] = LAMBDA x : f1(x) - f2(x); *(b,f1) : MACRO [T -> Vect2] = LAMBDA x : b*f1(x); %% scalar product *(r,f) : [T -> Vect2] = LAMBDA (t:T): r(t)*f(t); *(f1,f2) : MACRO [T -> real] = LAMBDA x : f1(x)*f2(x); %% dot product const_vfun(a) : MACRO [T -> Vect2] = (LAMBDA x : (a,a)) const_vfun(v) : [T -> Vect2] = (LAMBDA x : v) ; %------------------ % Rewrite rules %------------------ diff_function : LEMMA f1 - f2 = f1 + (- f2) negneg_function : LEMMA - (- f1) = f1 END vect_fun_ops_rv ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28