Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sqrt_rew.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.