| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
SSL complex_sets.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Set-valued complex functions % % Author: David Lester, Manchester University & NIA % % Version 1.0 4/12/07 Initial version (DRL) %------------------------------------------------------------------------------ complex_sets: THEORY BEGIN IMPORTING exp z,z1,z2: VAR complex n0x,n0y,n0z: VAR nzcomplex nnx: VAR nnreal nx: VAR negreal r,x,y: VAR real j: VAR int theta: VAR argrng % Considerable notational and practical convenience can be obtained by using % instead "Arg" to represent the set of all possible argument values. % To bring elegance into this theory we define addition and unary and % binary minus. ; -: MACRO [nonempty_set[real]->nonempty_set[real]] = (LAMBDA (X:nonempty_set[real]): {x | X(-x)}); +: MACRO [nonempty_set[real],nonempty_set[real]->nonempty_set[real]] = (LAMBDA (X,Y:nonempty_set[real]): {z:real | EXISTS (x:(X),y:(Y)): z = x+y}); -: MACRO [nonempty_set[real],nonempty_set[real]->nonempty_set[real]] = (LAMBDA (X,Y:nonempty_set[real]): {z:real | EXISTS (x:(X),y:(Y)): z = x-y}); Arg(n0z): nonempty_set[real] = {x:real | EXISTS j: x = arg(n0z) + 2*j*pi} Arg_def: LEMMA Arg(n0z) = {x:real | abs(n0z)*exp(x*i) = n0z} Arg_mult: LEMMA Arg(n0x*n0y) = Arg(n0x) + Arg(n0y) Arg_inv: LEMMA Arg(1/n0z) = -Arg(n0z) Arg_div: LEMMA Arg(n0x/n0y) = Arg(n0x) - Arg(n0y) END complex_sets ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28