| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Sequents/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 5 kB |
|
Quellcode-Bibliothek graph_path_conn.pvs Sprache: PVS |
|||||||||
|
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 ¤ 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.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
