subtrees[T: TYPE]: THEORY 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 < l(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 < l(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) max_tree_all_verts: LEMMA path_connected?(G) IMPLIES vert(max_subtree(G)) = vert(G) END subtrees