Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: number_sign_changes.prf Sprache: PVS

Original von: 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.18 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.