max_subtrees[T: TYPE]: THEORY BEGIN IMPORTING trees[T] G: VAR Digraph[T] % not empty?(G) IMPORTING max_di_subgraphs[T], doubletons[T] v: VAR T sing_is_tree: LEMMA tree?[T](singleton_digraph(v)) tree_in: LEMMA (EXISTS (Tr: Tree[T]): di_subgraph?(Tr,G) AND nonempty?[T](vert(Tr))) Tr,S: VAR Tree[T] Subtree(G: digraph[T]): TYPE = {Tr: Tree | di_subgraph?(Tr,G)} max_subtree(G: Digraph[T]): Subtree(G) = max_di_subgraph(G,(LAMBDA G: tree?(G))) max_subtree_tree : LEMMA tree?(max_subtree(G)) max_subtree_di_subgraph: LEMMA di_subgraph?(max_subtree(G),G) max_subtree_max : LEMMA FORALL (SS: Subtree(G)): size(SS) <= size(max_subtree(G)) END max_subtrees