path_lems[T: TYPE]: THEORY BEGIN IMPORTING paths[T] G: VAR digraph[T] cycle?(G: digraph[T], (w: Seq(G))): bool = pre_circuit?(G,w) AND l(w) > 1 AND w(1) /= w(l(w)-2) AND (FORALL (i,j: below(l(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 l(w) > 3) cycle_has_path: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IMPLIES (EXISTS (j: below(l(w))): path?(G,w^(0,j))) % fslib: LIBRARY = "../lib/fs/" % % IMPORTING digraphs, fslib@finite_sets_card_eq, seq_pidgeon IMPORTING digraphs, finite_sets_card_eq, seq_pidgeon GF: VAR Digraph[T] Pigeon_hole: THEOREM FORALL (w: Walk(GF)): l(w) > card(vert(GF)) IMPLIES (EXISTS (i,j: below(l(w))): i /= j AND w(i) = w(j)) END path_lems