Quelle sqrt_rew.pvs Sprache: PVS

sqrt_rew: THEORY
%------------------------------------------------------------------------
%
%  Square root AUTO-REWRITE+ definitions to increase automation
%
%------------------------------------------------------------------------

BEGIN

  IMPORTING sqrt, sq_rew

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

  AUTO_REWRITE+   sqrt_0         %  : LEMMA  sqrt(0) = 0
  AUTO_REWRITE+   sqrt_1         %  : LEMMA  sqrt(1) = 1

  AUTO_REWRITE+   sqrt_eq_0      %  : LEMMA  sqrt(nnx) = 0 IMPLIES nnx = 0
  AUTO_REWRITE+   sqrt_def       %  : LEMMA  sqrt(nnx) * sqrt(nnx) = nnx
  AUTO_REWRITE+   sqrt_square    %  : LEMMA  sqrt(nnx * nnx) = nnx

  AUTO_REWRITE+   sqrt_sq        %  : LEMMA  x >= 0 IMPLIES sqrt(sq(x)) = x
  AUTO_REWRITE+   sqrt_sq_neg    %  : LEMMA  x < 0 IMPLIES sqrt(sq(x)) = -x
  AUTO_REWRITE+   sqrt_sq_abs    %  : LEMMA  sqrt(sq(x)) = abs(x)

  sqrt_4              : LEMMA  sqrt(4) = 2
  sqrt_9              : LEMMA  sqrt(9) = 3
  sqrt_16             : LEMMA  sqrt(16) = 4
  sqrt_25             : LEMMA  sqrt(25) = 5
  sqrt_36             : LEMMA  sqrt(36) = 6
  sqrt_49             : LEMMA  sqrt(49) = 7
  sqrt_64             : LEMMA  sqrt(64) = 8
  sqrt_81             : LEMMA  sqrt(81) = 9
  sqrt_100            : LEMMA  sqrt(100) = 10

  AUTO_REWRITE+   sqrt_4
  AUTO_REWRITE+   sqrt_9
  AUTO_REWRITE+   sqrt_16
  AUTO_REWRITE+   sqrt_25
  AUTO_REWRITE+   sqrt_36
  AUTO_REWRITE+   sqrt_49
  AUTO_REWRITE+   sqrt_64
  AUTO_REWRITE+   sqrt_81
  AUTO_REWRITE+   sqrt_100

  sqrt_factor_left  : LEMMA  sqrt(nna * nnx * nnx) = sqrt(nna) * nnx
  sqrt_factor_middle: LEMMA  sqrt(nnx * nna * nnx) = sqrt(nna) * nnx
  sqrt_factor_right : LEMMA  sqrt(nnx * nnx * nna) = sqrt(nna) * nnx

  AUTO_REWRITE+   sqrt_factor_left
  AUTO_REWRITE+   sqrt_factor_middle
  AUTO_REWRITE+   sqrt_factor_right

%  sqrt_times_rev  : LEMMA  sqrt(nny) * sqrt(nnz) = sqrt(nny * nnz)

%  sqrt_div_rev    : LEMMA  nnz /= 0 IMPLIES
%                              sqrt(nny) / sqrt(nnz) = sqrt(nny / nnz)

%  AUTO_REWRITE+   sqrt_times_rev
%  AUTO_REWRITE+   sqrt_div_rev

END sqrt_rew

quality100%

¤ Dauer der Verarbeitung: 0.12 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.