| 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 root.pvs Sprache: PVS |
|||||||||
|
root: THEORY
% Computes nth root % % Narkawicz 12/13 % BEGIN r,x,y: VAR real n: VAR posnat epsil,delta: VAR posreal f,g : VAR [real->real] nnr,nnx: VAR nnreal m : VAR nat mult_expt_pos: LEMMA (x*y)^n = x^n*y^n real_mult_cont: LEMMA (FORALL (epsil,x): EXISTS (delta): FORALL (y): abs(x-y)<delta IMPLIES abs(f(x)-f(y))<epsil) AND (FORALL (epsil,x): EXISTS (delta): FORALL (y): abs(x-y)<delta IMPLIES abs(g(x)-g(y))<epsil) IMPLIES (FORALL (epsil,x): EXISTS (delta): FORALL (y): abs(x-y)<delta IMPLIES abs(f(x)*g(x)-f(y)*g(y))<epsil) expt_increasing: LEMMA nnr<=nnx IMPLIES nnr^m<=nnx^m expt_cont: LEMMA EXISTS (delta): FORALL (y): abs(x-y)<=delta IMPLIES abs(x^n-y^n)<epsil nn_root_exists: LEMMA EXISTS (nnx): nnx^n=nnr root_pos(nnr,n): {nnx|nnx^n=nnr} root_real(r)(n|r>=0 OR odd?(n)): {x | (x=0 IFF r = 0) AND (x>0 IFF r>0) AND (x<0 IFF r<0) AND (x>=0 IFF r>=0) AND (x<=0 IFF r<=0) AND x^n = r} = IF r=0 THEN 0 ELSIF r>0 THEN root_pos(r,n) ELSE -1*root_pos(-r,n) ENDIF END root ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28