subtrees[T: TYPE]: THEORY
BEGIN

   IMPORTING max_subtrees[T], graph_conn_defs[T]

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

   S: VAR graph[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 doubleton[T]
    v,w: VAR T
    add_dbl: LEMMA  vert(G)(v) AND v /= w AND
                 add(dbl[T](v, w), edges(G))(e)
              IMPLIES (FORALL (x: T): e(x) IMPLIES add(w, vert(G))(x))

    max_tree_all_verts: LEMMA path_connected?(G)   IMPLIES
                               vert(max_subtree(G)) = vert(G)


END subtrees