Quelle  max_subtrees.pvs

max_subtrees[T: TYPE]: THEORY
BEGIN

   IMPORTING trees[T]

   G: VAR Graph[T]    % not empty?(G)

   IMPORTING  max_subgraphs[T]

   v: VAR T
   sing_is_tree: LEMMA tree?[T](singleton_graph(v))

   tree_in: LEMMA (EXISTS (Tr: Tree[T]): subgraph?(Tr,G) AND
                          nonempty?[T](vert(Tr)))

   Tr,S: VAR Tree[T]

   Subtree(G: graph[T]): TYPE = {Tr: Tree | subgraph?(Tr,G)}

   max_subtree(G: Graph[T]): Subtree(G) = max_subgraph(G,(LAMBDA G: tree?(G)))

   max_subtree_tree    : LEMMA tree?(max_subtree(G)) 

   max_subtree_subgraph: LEMMA subgraph?(max_subtree(G),G)

   max_subtree_max     : LEMMA FORALL (SS: Subtree(G)): 
                                         size(SS) <= size(max_subtree(G)) 

END max_subtrees