cycles[T: TYPE]: THEORY

BEGIN

   IMPORTING paths[T]

   G: VAR graph[T]


   cycle?(G: graph[T], (w: Seq(G))): bool = pre_circuit?(G,w) AND length(w) > 1 AND 
                          w(1) /= w(length(w)-2) AND
                          (FORALL (i,j: below(length(w))):
                             w(i) = w(j) IMPLIES (i = j OR 
                                         (endpoint?(i,w) AND endpoint?(j,w)))) 

   cycle_l_gt_3: LEMMA (FORALL (w: Seq(G)): cycle?(G,w) IMPLIES length(w) > 3)



   cycle_has_path: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IMPLIES
                            (EXISTS (j: below(length(w))): path?(G,w^(0,j)))


%% -- the term "w(1) /= w(length(w)-2)" rules out length(w) = 2 AND length(w) = 3 --
   

   cycle_gt3: LEMMA FORALL (w: Seq(G)):  cycle?(G,w) IMPLIES length(w) > 3

   cycle_def: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IFF
                          pre_circuit?(G,w) AND length(w) > 3 AND 
                          (FORALL (i,j: below(length(w))):
                             w(i) = w(j) IMPLIES (i = j OR 
                                         (endpoint?(i,w) AND endpoint?(j,w))))
                       



END cycles