Quelle  path_lems.pvs

path_lems[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   IMPORTING graphs, finite_sets@finite_sets_card_eq, 
             structures@seq_pigeon

   GF: VAR Graph[T]

   Pigeon_hole: THEOREM FORALL (w: Walk(GF)): length(w) > card(vert(GF)) IMPLIES 
                  (EXISTS (i,j: below(length(w))): i /= j AND w(i) = w(j))
   

END path_lems