trees[T: TYPE]: THEORY BEGIN IMPORTING graph_deg[T], graph_ops[T], subgraphs[T] G,GP,C,GG: VAR graph[T] tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR (EXISTS (v: (vert(G))): deg(v,G) = 1 AND tree?(del_vert[T](G,v))) MEASURE size(G) tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G) Tree: TYPE = {G: graph[T] | tree?(G)} END trees