products/sources/formale Sprachen/PVS/reals/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: derivatives.prf   Sprache: PVS

Original von: PVS©
sqrt_exists: THEORY
%--------------------------------------------------------------------------------
%
%   This theory provides a non-constructive proof of the existence of the
%   square root function.  The proof has been adapted from Rosenlicht's
%   Introduction to Analysis.
%
%--------------------------------------------------------------------------------


BEGIN
  
  e: VAR posreal
  x, y: VAR real
  nnx, nny: VAR nonneg_real
  i: var posnat
  
  epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y

  expt_0       : LEMMA 0^i = 0

  lt1_expt_le  : LEMMA nnx < 1 => nnx^i <= nnx

  sqrt_exists  : LEMMA
                   EXISTS (x1: [nnx: nonneg_real -> {nny | nny*nny = nnx}]): TRUE

END sqrt_exists



¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff