| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle appendix.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Appoximation results % % Author: David Lester, Manchester University % % Version 1.0 18/2/09 Initial Release Version %------------------------------------------------------------------------------ appendix: THEORY BEGIN IMPORTING prelude_aux, prelude_A4, reals@sqrt n,m: VAR nat i,p,r: VAR int pn,q: VAR posnat px,py: VAR posreal x,e1,e2: VAR real lemma_A1: LEMMA m*m <= n AND n < (m+1)*(m+1) IFF m = floor(sqrt(n)) lemma_A2: LEMMA r = round(p/q) IFF (r-1/2)*q <= p AND p < (r+1/2)*q lemma_A3: LEMMA i = floor(log2(px)) IFF 2^i <= px AND px < 2^(i+1) lemma_A4: LEMMA e1 = 2^ -(n+floor(log2(pn))+2) AND e2 = 2^ -n AND -1 < x AND x < 1 => x^pn-e2 < (x-e1)^pn AND x^pn-e2 < (x+e1)^pn AND (x-e1)^pn < x^pn+e2 AND (x+e1)^pn < x^pn+e2 epsilon_log2_aux: LEMMA FORALL (n:posnat): EXISTS (p:nat): n < 2^p epsilon_log2: LEMMA EXISTS (p:nat): 1/2^p < px floor_sqrt_aux(n,m:nat): RECURSIVE nat = (IF (m+1)*(m+1) <= n THEN 1+floor_sqrt_aux(n,m+1) ELSE 0 ENDIF) MEASURE (LAMBDA n,m: (IF n >= (m+1)*(m+1) THEN n-m ELSE 0 ENDIF)) floor_sqrt(n:nat): nat = floor_sqrt_aux(n,0) floor_sqrt_def: LEMMA floor_sqrt(n) = floor(sqrt(n)) floor_log2(n:posnat): RECURSIVE nat = (IF n >= 2 THEN 1 + floor_log2(floor(n/2)) ELSE 0 ENDIF) MEASURE (LAMBDA n:n) floor_log2_def: LEMMA floor_log2(pn) = floor(log2(pn)) END appendix ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28