trees[T: TYPE]: THEORY BEGIN IMPORTING digraph_deg[T], digraph_ops[T], di_subgraphs[T] G,GP,C,GG: VAR digraph[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: digraph[T] | tree?(G)} END trees