SSL reduction.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: September 29, 2009                                      
%%                                                                          
%%----------------------------------------------------------------------------


reduction[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 rewrite_rules[variable,symbol, arity]            
                        

   s, t, t1, t2: VAR term
sigma, sg1, sg2: VAR Sub
              x: VAR (V)
              R: VAR pred[[term, term]] 
              E: VAR set[rewrite_rule]
              e: VAR rewrite_rule


%%%% Defining, respectively, the concepts Reduction relation and closed under %%
%%%% substitutions,Close under substitution                                   %%

 reduction?(E)(s,t): bool =  
     EXISTS ( (e | member(e, E)), sigma, (p: positions?(s))): 
                      subtermOF(s, p) = ext(sigma)(lhs(e)) & 
                                    t = replaceTerm(s, ext(sigma)(rhs(e)), p)


 close_subs?(R): bool = FORALL s, t, sigma: R(s,t) => 
                                            R(ext(sigma)(s),ext(sigma)(t))


%%%% Properties %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 closure_close_subs: LEMMA close_subs?(R)  =>
                (close_subs?(TC(R)) & close_subs?(RTC(R)) & close_subs?(EC(R)))

 reduction_is_subs_op: LEMMA close_subs?(reduction?(E)) & comp_op?(reduction?(E))

 lhs_reduces_to_rhs: LEMMA
                    FORALL (E, (e | member(e, E))): reduction?(E)(lhs(e), rhs(e))

END reduction