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
% [email protected]
%-------------------------------------------------------------------------------
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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
