Quelle  tree_circ.pvs

tree_circ[T: TYPE]: THEORY
BEGIN

   IMPORTING trees[T], graphs[T], graph_deg[T], graph_ops[T],
             circuit_deg[T], subgraphs_from_walk[T]  

   G,GP,C,GG: VAR graph[T]

   GT: VAR Tree

   IMPORTING abstract_min

   exists_c_tree: LEMMA FORALL (w: Walk(GT)): 
                              EXISTS (t: Tree[T]): subgraph?(G_from(GT, w), t)

   c_tree(TR: Tree, C: Subgraph(TR)): Tree =
            min[Tree[T],(LAMBDA GT: size(GT)),
                         (LAMBDA GT: subgraph?(C,GT))]

   tree_containing_lem: LEMMA FORALL (w: Walk(GT)): 
         tree?(c_tree(GT,G_from(GT,w))) AND
         subgraph?(G_from(GT,w),c_tree(GT,G_from(GT,w))) AND
         (FORALL (GG: Tree): subgraph?(G_from(GT,w),GG) IMPLIES
                                 size(c_tree(GT,G_from(GT,w))) <= size(GG))

   tree_deg: LEMMA FORALL (w: Walk(GT), v: T): 
                 vert(c_tree(GT,G_from(GT,w)))(v) AND 
                 deg(v, G_from(GT,w)) >= 2
                     IMPLIES  deg(v, c_tree(GT,G_from(GT,w))) >= 2

   small_tree_lem: LEMMA FORALL (w: Walk(G)): tree?(G) =>
                                 size(G) <= 1 IMPLIES NOT circuit?(G,w)

   tree_no_circuits: THEOREM (FORALL (w: Walk(G)): tree?(G) =>
                                   NOT circuit?(G,w))


END tree_circ