Quelle  noetherian.pvs   Sprache: 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: December 02, 2006                                      
%%                                                                          
%%---------------------------------------------------------------------------


noetherian[T : TYPE] : THEORY
BEGIN

  IMPORTING ars_terminology[T], 
            orders@well_foundedness[T]
  
     P : VAR PRED[T]
     R : VAR PRED[[T, T]]
  x, y : VAR T


%%------------------------** Termination (Noetherian) **--------------------
%%
%% A reduction -> (relation R) is
%%
%% - noetherian (terminating) iff there is no infinite
%%   descending  chain a0 -> a1 -> .... In other words, a relation -> is 
%%   noetherian if the inverse (converse) relation of -> is well founded.
%%
%% - convergent if is confluent and noetherian.
%%
%% - R_is_Noet_iff_TC_is: ->+ is terminating iff -> is.
%%
%%
%% - noetherian_induction: To prove P(x) for all x, it suffices to prove P(x)
%%                         under the assunption that P(y) holds for all 
%%                         successors y of x. 
%%
%%--------------------------------------------------------------------------

 
 noetherian?(R): bool = well_founded?(converse(R))


 noetherian: TYPE = (noetherian?)


 convergent?(R): bool = confluent?(R) & noetherian?(R)


 R_is_Noet_iff_TC_is: LEMMA noetherian?(R) <=> noetherian?(TC(R))
 

 noetherian_induction: LEMMA 
             (FORALL (R: noetherian, P):
               (FORALL x: 
                  (FORALL y: TC(R)(x, y) IMPLIES P(y)) 
                      IMPLIES P(x))
            IMPLIES
              (FORALL x: P(x)))


END noetherian