Quelle  subtrees.pvs

subtrees[T: TYPE]: THEORY
%-------------------------------------------------------------------------------
%  Authors:
%
%      Ricky W. Butler,    NASA Langley
%      Kristin Y. Rozier,  NASA Langley
%
%  Last modified 07/30/04
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center   
%                        R.W.Butler@larc.nasa.gov
%-------------------------------------------------------------------------------
BEGIN

   IMPORTING max_subtrees[T], digraph_conn_defs[T]

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

   S: VAR digraph[T]

   n: VAR nat 
   walk_acr: LEMMA FORALL (w: Walk(G)): n < length(w) AND
                                vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n))
                               IMPLIES
                    (EXISTS (j: posnat): (j <= n
                      AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j)))))


   walk_acr2: LEMMA FORALL (w: Walk(G)): n < length(w) AND
                                vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n))
                               IMPLIES
                    (EXISTS (j: posnat): (j <= n
                      AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j)))))

    e: VAR edgetype[T]
    v,w: VAR T
    add_pair: LEMMA  vert(G)(v) AND v /= w AND
                 add((v, w), edges(G))(e)
              IMPLIES 
                 LET (x,y) = e IN add(w, vert(G))(x) AND add(w, vert(G))(y)


    no_self_loops?(G): bool = FORALL (e: (edges(G))): e`1 /= e`2

    max_tree_all_verts: LEMMA connected?(G) AND
                              no_self_loops?(G)
                           IMPLIES
                               vert(max_subtree(G)) = vert(G)

%Another possible lemma: (after a definition for root exists)
% Starting from the root, there exists a walk from the root to
% any other vertex in G

END subtrees