Quelle  sqrt_rew.pvs   Sprache: unbekannt

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%

[ zur Elbe Produktseite wechseln0.11Quellennavigators  Analyse erneut starten  ]