| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle complex_sqrt.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Sqrare root properties of Complex Numbers. % % Author: David Lester, Manchester University % % Version 1.0 4/11/07 Initial version (DRL) %------------------------------------------------------------------------------ complex_sqrt: THEORY BEGIN IMPORTING polar, trig@trig_basic, number_fields_sq nnx: VAR nnreal npx: VAR npreal x,y,z: VAR complex n0x,n0y,n0z: VAR nzcomplex sqrt(z):complex = from_polar(sqrt(abs(z)),arg(z)/2) sqrt_nz_is_nz : JUDGEMENT sqrt(n0z) HAS_TYPE nzcomplex sqrt_nnz : LEMMA sqrt(nnx) = sqrt.sqrt(nnx) sqrt_npz : LEMMA sqrt(npx) = i*sqrt.sqrt(-npx) sqrt_0 : LEMMA sqrt(0) = 0 sqrt_1 : LEMMA sqrt(1) = 1 sqrt_neg1 : LEMMA sqrt(-1) = i sqrt_eq_0 : LEMMA sqrt(z) = 0 IFF z = 0 sqrt_sq : LEMMA sqrt(sq(z)) = IF -pi/2 < arg(z) AND arg(z) <= pi/2 THEN z ELSE -z ENDIF sq_sqrt : LEMMA sq(sqrt(z)) = z sqrt_times: LEMMA sqrt(x*y) = IF -pi < arg(x)+arg(y) AND arg(x)+arg(y) <= pi THEN sqrt(x)*sqrt(y) ELSE -sqrt(x)*sqrt(y) ENDIF sqrt_neg : LEMMA sqrt(-z) = IF arg(z) <= 0 THEN i*sqrt(z) ELSE -i*sqrt(z) ENDIF sqrt_inv : LEMMA sqrt(1/n0z) = IF arg(n0z) = pi THEN -1/sqrt(n0z) ELSE 1/sqrt(n0z) ENDIF sqrt_div : LEMMA sqrt(x/n0y) = IF (arg(n0y) = pi & arg(x) > 0) OR arg(n0y) = 0 OR (-pi < arg(x)-arg(n0y) & arg(x)-arg(n0y) <= pi) THEN sqrt(x) / sqrt(n0y) ELSE -sqrt(x) / sqrt(n0y) ENDIF END complex_sqrt ¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28