Quelle  compatibility.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                                      
%%                                                                          
%%----------------------------------------------------------------------------


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

 BEGIN

  IMPORTING replacement[variable,symbol, arity], 
            finite_sets[(V)] as fsetvar,
            ars[term]
            

      r, s, t: VAR term
            R: VAR pred[[term, term]]
            x: VAR (V)
            n: VAR nat



%%%% Defining the set of all function symbols whose arity is n %%%%%%%%%%%%%%%%%

  arity_eq(n): TYPE = {f: symbol | arity(f) = n}



%%%% Defining, respectively, the concepts closed under operations, compatible %% 
%%%% with operations, and compatible with contexts                            %%

 close_op?(R): bool = 
    FORALL ( n: nat, (f: arity_eq(n)), (st1, st2: fset.fs_len(n))):
      (FORALL (m: below[n]): R(st1(m), st2(m))
         => R(app(f, st1), app(f, st2)))

      
 comp_op?(R): bool = 
    FORALL (n: nat, i: below[n], (f: arity_eq(n)), (st1: fset.fs_len(n)), t):
       LET s = st1(i), st2 = replace(t, st1, i) IN
         R(s,t) =>  R(app(f,st1), app(f,st2))


 comp_cont?(R): bool = FORALL (p: position), s: positionsOF(s)(p) =>
                        (FORALL r, t: R(r,t) =>  
                           R(replaceTerm(s, r, p), replaceTerm(s, t, p)))



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


 comp_op_iff_comp_cont: LEMMA comp_op?(R) <=> comp_cont?(R)


 closure_comp_op: LEMMA comp_op?(R) => 
                 (comp_op?(TC(R)) & comp_op?(RTC(R)) & comp_op?(EC(R)))

 closure_comp_cont: LEMMA comp_cont?(R) => 
                 (comp_cont?(TC(R)) & comp_cont?(RTC(R)) & comp_cont?(EC(R)))

 END compatibility