|
graph_conn_defs[T: TYPE]: THEORY
BEGIN
IMPORTING graph_deg[T]
G,G1,G2: VAR graph[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)
IMPORTING walks[T]
path_connected?(G): bool = NOT empty?(G) AND
(FORALL (x,y: (vert(G))): % x /= y IMPLIES
(EXISTS (w: Walk(G)): seq(w)(0) = x AND
seq(w)(length(w)-1) = y))
H1,H2: VAR graph[T]
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
END graph_conn_defs
¤ Dauer der Verarbeitung: 0.0 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.
|
