Quellcode-Bibliothek prelude_sqrt.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Definition and properties of sqrt
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

prelude_sqrt: THEORY

  BEGIN
  IMPORTING prelude_aux

  nnx,nny,nnz: VAR nnreal
  px,py,pz:    VAR posreal
  y,w:         VAR real

  square_le1: LEMMA nnx*nnx <= (nnx+nny)*(nnx+nny)
  square_le2: LEMMA nnx*nnx <= 1       <=> nnx <= 1
  square_le3: LEMMA nnx*nnx < nny*nny  <=> nnx < nny
  square_eq1: LEMMA nnx*nnx = nny*nny  <=> nnx = nny
  square_le4: LEMMA nnx*nnx <= nny*nny <=> nnx <= nny
  square_le5: LEMMA 1 < px*px          <=> 1 < px
  square_le6: LEMMA nnx*nnx <= py AND 1 < py => nnx < py

  square_archimedean1: LEMMA EXISTS (n:posnat): 1/(n*n) < px
  square_archimedean2: LEMMA EXISTS (n:posnat): 2/n + 1/(n*n) < px

  square_exist_lt1: LEMMA py <= 1 AND py*py < px =>
                          EXISTS pz: py < pz AND pz*pz < px
  square_exist_lt2: LEMMA EXISTS pz: pz*pz < px
  square_exist_lt3: LEMMA nny*nny < px => EXISTS pz: nny < pz AND  pz*pz < px

  square_exist_gt3: LEMMA nnx < py*py =>
                          EXISTS nnz: nnz < py AND  nnx < nnz*nnz

  sqrt_set(nnx:nnreal):setof[nnreal] = {y | y*y <= nnx}

  sqrt_set_UB(nnx:nnreal):nnreal = IF nnx <= 1 THEN 1 ELSE nnx ENDIF

  sqrt_set_nonempty: LEMMA nonempty?(sqrt_set(nnx))
  sqrt_set_has_UB: LEMMA upper_bound?(sqrt_set_UB(nnx),sqrt_set(nnx))
  sqrt_set_LUB: LEMMA nny*nny = nnx <=> least_upper_bound?(nny,sqrt_set(nnx))

  square(nnx:nnreal):nnreal = nnx*nnx

  square_injective:  LEMMA injective?(square)

  square_surjective: LEMMA surjective?(square)
  square_bijective:  LEMMA bijective?(square)

  sqrt:[nnreal->nnreal] = inverse(square)

  square_is:    LEMMA square(nnx) = nnx*nnx
  sqrt_square1: LEMMA square(sqrt(nnx))=nnx
  sqrt_square2: LEMMA sqrt(square(nnx))=nnx
  square_times: LEMMA square(nnx*nny) = square(nnx)*square(nny)
  sqrt_times:   LEMMA sqrt(nnx)*sqrt(nny) = sqrt(nnx*nny)
  sqrt_zero:    LEMMA sqrt(0) = 0
  sqrt_one:     LEMMA sqrt(1) = 1
  both_sides_sqrt1:    LEMMA sqrt(nnx) =  nny       <=> nnx     =  nny*nny
  both_sides_sqrt2:    LEMMA sqrt(nnx) =  sqrt(nny) <=> nnx     =  nny
  both_sides_sqrt_lt1: LEMMA sqrt(nnx) <  nny       <=> nnx     <  nny*nny
  both_sides_sqrt_lt2: LEMMA sqrt(nnx) <  sqrt(nny) <=> nnx     <  nny
  both_sides_sqrt_lt3: LEMMA nnx       <  sqrt(nny) <=> nnx*nnx <  nny
  both_sides_sqrt_le1: LEMMA sqrt(nnx) <= nny       <=> nnx     <= nny*nny
  both_sides_sqrt_le2: LEMMA sqrt(nnx) <= sqrt(nny) <=> nnx     <= nny
  both_sides_sqrt_le3: LEMMA nnx       <= sqrt(nny) <=> nnx*nnx <= nny

  END prelude_sqrt

quality93%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.