|
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
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
