Quellcode-Bibliothek vectors_3D_rew.pvs   Sprache: unbekannt

vectors_3D_rew : THEORY

%
% NOTE:  USE "auto_rewrite_theory "vectors_3D_rew"
%        If want distributed property applied also USE
%             "auto_rewrite_theory "vectors_dist"

BEGIN

  IMPORTING vectors_3D

  u,v,w    : VAR Vect3
  a,b      : VAR real


  AUTO_REWRITE+ vx_distr_add
  AUTO_REWRITE+ vy_distr_add
  AUTO_REWRITE+ vz_distr_add
  AUTO_REWRITE+ vx_distr_sub
  AUTO_REWRITE+ vy_distr_sub
  AUTO_REWRITE+ vz_distr_sub

  AUTO_REWRITE+ vx_scal                %% NEW %%
  AUTO_REWRITE+ vy_scal                %% NEW %%
  AUTO_REWRITE+ vz_scal                %% NEW %%

  AUTO_REWRITE+ sqv_scal
  AUTO_REWRITE+ norm_scal

  AUTO_REWRITE+ neg_distr_sub  
  AUTO_REWRITE+ neg_distr_add  
  AUTO_REWRITE+ dot_add_right  
  AUTO_REWRITE+ dot_add_left 
  AUTO_REWRITE+ dot_sub_right  
  AUTO_REWRITE+ dot_sub_left 
  AUTO_REWRITE+ scal_add_left      
  AUTO_REWRITE+ scal_sub_left  
  AUTO_REWRITE+ scal_add_right
  AUTO_REWRITE+ scal_sub_right


%  AUTO_REWRITE+  sqv_add        
%  AUTO_REWRITE+  sqv_sub        


END vectors_3D_rew