trs.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: October 15, 2008                                      

%%                                                                          
%%----------------------------------------------------------------------------


trs[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 critical_pairs[variable,symbol, arity]

  END trs