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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
