|
graph_path_conn[T: TYPE]: THEORY
BEGIN
IMPORTING graph_conn_defs[T], walks[T], subgraphs[T]
G,G1,G2: VAR graph[T]
isolated_not_path: LEMMA isolated?(G) AND NOT singleton?(G)
IMPLIES NOT path_connected?(G)
u,v,y: VAR T
pic_A: LEMMA (EXISTS v: vert(G)(v) AND deg(v,G) = 0)
IMPLIES path_connected?(G) IMPLIES connected?(G)
IMPORTING graph_inductions[T], subtrees[T], path_ops[T]
thw_A: LEMMA (FORALL (GG: graph[T]): size(GG) < size(G)
IMPLIES
(FORALL (x: T, y: T): tree?(GG) AND vert(GG)(x)
AND vert(GG)(y) AND x /= y
IMPLIES (EXISTS (w: Walk(GG)): walk_from?(GG, w, x, y))))
AND deg(v, G) = 1 AND tree?(del_vert[T](G, v)) AND
vert(G)(v) AND vert(G)(y) AND v /= y
IMPLIES
(EXISTS (w: Walk(G)): walk_from?(G, w, v, y))
TR: VAR graph[T]
x: VAR T
tree_has_walk: LEMMA tree?(TR) AND vert(TR)(x) AND vert(TR)(y)
AND x /= y IMPLIES
(EXISTS (w: Walk(TR)):
walk_from?(TR,w,x,y))
path_implies_conn: THEOREM path_connected?(G) IMPLIES connected?(G)
END graph_path_conn
¤ 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.
|
