Quelle  walk_inductions.pvs

walk_inductions[T: TYPE]: THEORY
BEGIN

   IMPORTING walks[T]

   P: VAR pred[prewalk]
   n: VAR nat
   w,ww: VAR prewalk

   walk_prep              : LEMMA (FORALL w: P(w)) IFF 
                                       (FORALL n, w : length(w) = n IMPLIES P(w)) 
   
   
   graph_induction_walk    : THEOREM (FORALL w:
                                 (FORALL ww: length(ww) < length(w) IMPLIES P(ww))
                                                 IMPLIES P(w))
                                   IMPLIES (FORALL w: P(w))
    
END walk_inductions