Quelle  extending_rename.pvs   Sprache: PVS

%%-------------------** Term Rewriting System (TRS) **------------------------
%%                                                                          
%% Authors         : Andre Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and 
%%
%%                   Mauricio Ayala Rincon  
%%                   Universidade de Brasília - Brasil  
%%                   
%% Last Modified On: March 24, 2008                                      
%%                                                                          
%%----------------------------------------------------------------------------


extending_rename[T:TYPE]: THEORY
 BEGIN

 
  S, R: VAR set[T]
     t: VAR T

  extend_to_identity((S),(R),(f:(bijective?[(S),(R)])))(t): T = 
        IF S(t) THEN f(t)
        ELSE 
          t 
        ENDIF

 END extending_rename