|
graph_connected[T: TYPE]: THEORY
BEGIN
IMPORTING graph_ops[T], graph_deg[T], walks[T],
graph_conn_defs[T],
graph_conn_piece, graph_piece_path, % FOR PROOF ONLY
graph_path_conn, graph_complected % FOR PROOF ONLY
G,G1,G2,H1,H2: VAR graph[T]
conn_eq_path : THEOREM connected?(G) = path_connected?(G)
path_eq_piece : THEOREM path_connected?(G) = piece_connected?(G)
piece_eq_conn : THEOREM piece_connected?(G) = connected?(G)
conn_eq_complected : THEOREM connected?(G) = complected?(G)
%WHERE (defined in graph_conn_defs[T])
%
% connected?(G): RECURSIVE bool = singleton?(G) OR
% (EXISTS (v: (vert(G))): deg(v,G) > 0
% AND connected?(del_vert(G,v)))
% MEASURE size(G)
%
% path_connected?(G): bool = (FORALL (x,y: (vert(G))): x /= y IMPLIES
% (EXISTS (w: Walk(G)): seq(w)(0) = x AND
% seq(w)(length(w)-1) = y))
%
% piece_connected?(G): bool = NOT empty?(G) AND
% (FORALL H1,H2: G = union(H1,H2) AND
% NOT empty?(H1) AND NOT empty?(H2)
% IMPLIES NOT empty?(intersection(vert(H1),
% vert(H2))))
%
% complected?(G): bool = IF isolated?(G) THEN singleton?(G)
% ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN
% (EXISTS (x: (vert(G))): deg(x,G) = 1 AND
% connected?(del_vert(G,x)))
% ELSE
% (EXISTS (e: (edges(G))):
% connected?(del_edge(G,e)))
% ENDIF
%
% are defined in graph_conn_defs.pvs
END graph_connected
¤ 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.
|
