Quellcode-Bibliothek modulo_equivalence.pvs

%%-------------------** Abstract Reduction System (ARS) **-------------------
%%                                                                          
%% 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                                      
%%                                                                          
%%---------------------------------------------------------------------------


modulo_equivalence[T : TYPE] : THEORY
BEGIN

  IMPORTING noetherian[T]

  R, S : VAR  PRED[[T, T]]
  Eq   : VAR equivalence
  x, y,
  z, w,
  u, v : VAR T

  R_Eq(R, Eq)  : PRED[[T, T]] = Eq o R o Eq

  SC_Eq(R, Eq) : PRED[[T, T]] = union(SC(R), Eq)

  Eq_Eq(R, Eq) : equivalence = EC(SC_Eq(R, Eq))

  joinable_m?(R, Eq)(x,y) : bool = EXISTS u,v: RTC(R)(x,u) & 
                                               Eq(u,v) & RTC(R)(y,v)

  church_rosser_m?(R, Eq) : bool = FORALL x, y: Eq_Eq(R, Eq)(x,y) => 
                                                joinable_m?(R, Eq)(x,y)
 
  local_confluent_m?(R, Eq) : bool = FORALL x, y, z: R(x,y) & R(x,z) => 
                                                     joinable_m?(R, Eq)(y,z)

  confluent_m?(R, Eq) : bool = FORALL x, y, z, w: RTC(R)(x,z)  & 
                                                  Eq(x,y) &
                                                  RTC(R)(y,w) => 
                                                  joinable_m?(R, Eq)(z,w)

  has_unique_nf_m?(R, Eq) : bool = FORALL x, y, u, v: is_normal_form?(R)(u) &
                                                      is_normal_form?(R)(v) &
                                                      RTC(R)(x,u) &
                                                      Eq_Eq(R, Eq)(x,y)  &
                                                      RTC(R)(y,v) => Eq(u,v)

  locally_coherent?(R, Eq, S) : bool = symmetric?(S) &
                                       FORALL  x, y, z: R(x,y) & 
                                       S(x,z) => joinable_m?(R, Eq)(y,z)

  noetherian_m?(R, Eq) : bool = well_founded?(converse(R o Eq))

  

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


van_oostrom94 : LEMMA diamond_property?(RTC(R) o Eq) => confluent_m?(R, Eq)


newman_lemma_general : THEOREM noetherian?(R) => 
                              (local_confluent_m?(R, Eq) & 
                               locally_coherent?(R, Eq, Eq) <=>  
                                                           confluent_m?(R, Eq))
            

END modulo_equivalence