Quelle sqrt.pvs Sprache: PVS

sqrt: THEORY
%------------------------------------------------------------------------
%
%  Square root of non-negative real
%
%  Supercedes older version: sqrt_ax
%
%  Authors:  Rick Butler             NASA
%            Cesar Munoz             NIA
%------------------------------------------------------------------------
BEGIN

  IMPORTING sq,sign,                      % sq(a): nonneg_real = a*a
            sqrt_exists

   nnx, nny, nnz: VAR nonneg_real
   a,x,y,z,xx: VAR real

  sqrt(nnx): {nnz : nnreal | nnz*nnz = nnx}

  sqrt_pos            : JUDGEMENT sqrt(px: posreal) HAS_TYPE posreal

% -------------------- Special Arguments --------------------

  sqrt_0              : LEMMA  sqrt(0) = 0
  sqrt_1              : LEMMA  sqrt(1) = 1
  sqrt_eq_0           : LEMMA  sqrt(nnx) = 0 IMPLIES nnx = 0
  sqrt_eq_1           : LEMMA  sqrt(nnx) = 1 IMPLIES nnx = 1

% -------------------- Basic Properties --------------------

  sqrt_lem            : LEMMA  sqrt(nny) = nnz IFF nnz * nnz = nny

  sqrt_def            : LEMMA  sqrt(nnx) * sqrt(nnx) = nnx

  sqrt_square         : LEMMA  sqrt(nnx * nnx) = nnx

  sqrt_sq             : LEMMA  x >= 0 IMPLIES sqrt(sq(x)) = x

  sqrt_sq_neg         : LEMMA  x < 0 IMPLIES sqrt(sq(x)) = -x

  sqrt_sq_abs         : LEMMA  sqrt(sq(x)) = abs(x)

  sqrt_sq_sign        : LEMMA  sqrt(sq(x)) = sign(x)*x

  sq_sqrt             : LEMMA  x >= 0 IMPLIES sq(sqrt(x))=x

  sqrt_times          : LEMMA  sqrt(nny * nnz) = sqrt(nny) * sqrt(nnz)

  sqrt_div            : LEMMA  nnz /= 0 IMPLIES
                                   sqrt(nny / nnz) = sqrt(nny) / sqrt(nnz)

  abs_sqrt            : LEMMA abs(sqrt(nnx)) = sqrt(nnx)

  sqrt_scal           : LEMMA abs(a)*sqrt(nnx) = sqrt(sq(a)*nnx)

% --------------------- Inequalities --------------------

  sqrt_lt             : LEMMA  sqrt(nny) < sqrt(nnz) IFF nny < nnz

  sqrt_le             : LEMMA  sqrt(nny) <= sqrt(nnz) IFF nny <= nnz

  sqrt_gt             : LEMMA  sqrt(nny) > sqrt(nnz) IFF nny > nnz

  sqrt_ge             : LEMMA  sqrt(nny) >= sqrt(nnz) IFF nny >= nnz

  sqrt_eq             : LEMMA  sqrt(nny) = sqrt(nnz) IFF nny = nnz

  sqrt_less           : LEMMA  nnx > 1 IMPLIES sqrt(nnx) < nnx

  sqrt_more           : LEMMA  nnx > 0 AND nnx < 1 IMPLIES sqrt(nnx) > nnx

  sqrt_lt_0           : LEMMA  nnx < 0 IFF sqrt(nnx) < 0

  sqrt_le_0           : LEMMA  nnx <= 0 IFF sqrt(nnx) <= 0

  sqrt_gt_0           : LEMMA  nnx > 0 IFF sqrt(nnx) > 0

  sqrt_ge_0           : LEMMA  nnx >= 0 IFF sqrt(nnx) >= 0

  sqrt_lt1            : LEMMA  nnx < 1 IFF sqrt(nnx) < 1

  sqrt_le1            : LEMMA  nnx <= 1 IFF sqrt(nnx) <= 1

  sqrt_gt1            : LEMMA  nnx > 1 IFF sqrt(nnx) > 1

  sqrt_ge1            : LEMMA  nnx >= 1 IFF sqrt(nnx) >= 1

  sqrt_plus_le        : LEMMA  sqrt(nnx+nny) <= sqrt(nnx) + sqrt(nny)

  sqrt_cauchy         : LEMMA FORALL (a,b,c,d: real):
                           a*c + b*d <= sqrt(sq(a)+sq(b)) *  sqrt(sq(c)+sq(d))

  sqrt_4              : LEMMA  sqrt(4) = 2
  sqrt_9              : LEMMA  sqrt(9) = 3
  sqrt_16             : LEMMA  sqrt(16) = 4
  sqrt_25             : LEMMA  sqrt(25) = 5

  AUTO_REWRITE+   sqrt_4
  AUTO_REWRITE+   sqrt_9
  AUTO_REWRITE+   sqrt_16
  AUTO_REWRITE+   sqrt_25

  AUTO_REWRITE+ sqrt_0
  AUTO_REWRITE+ sqrt_1
  AUTO_REWRITE+ sqrt_square
  AUTO_REWRITE+ sqrt_sq
  AUTO_REWRITE+ sqrt_sq_neg
  AUTO_REWRITE+ sq_sqrt

END sqrt

quality93%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.