%%-------------------** 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: September 29, 2009                                      
%%                                                                          
%%----------------------------------------------------------------------------


rewrite_rules[variable: TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY

 BEGIN

   ASSUMING
 
     IMPORTING variables_term[variable,symbol, arity],
               sets_aux@countability[term],
               sets_aux@countable_props[term]
 
       var_countable: ASSUMPTION is_countably_infinite(V)
      
   ENDASSUMING

     IMPORTING substitution[variable,symbol, arity]

  l, r: VAR term
   rho: VAR Ren 


%%%% Defining rewriting rules in agreement with Baader and Terese %%%%%%%%%%%%
    

 rewrite_rule?(l,r): bool = (NOT vars?(l)) & subset?(Vars(r), Vars(l))

 rewrite_rule: TYPE = (rewrite_rule?)

 ren_rewrite: LEMMA rewrite_rule?(l,r) => rewrite_rule?(ext(rho)(l),ext(rho)(r))



%%%% A subset of rewrite rules %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
           E: VAR set[rewrite_rule]

           e: VAR rewrite_rule
      lhs(e): term = e`1
      rhs(e): term = e`2


END rewrite_rules