cycle_deg[T: TYPE]: THEORY BEGIN IMPORTING path_lems[T], trees[T] G: VAR graph[T] n: VAR nat % **** NOT YET PROVED **** deg_gt_1_cycle: LEMMA (FORALL (v: T): vert(G)(v) IMPLIES deg(v,G) > 1) IMPLIES (EXISTS (C: Seq(G)): cycle?(G,C)) END cycle_deg