:: Trees: Connected, Acyclic Graphs :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSET_1, ARYTM_3, CARD_1, SUBSET_1, XBOOLE_0, GLIB_000, RELAT_2, GLIB_001, TREES_1, ZFMISC_1, FUNCT_1, FINSEQ_1, GRAPH_1, ABIAN, XXREAL_0, RELAT_1, RCOMP_1, FUNCOP_1, ARYTM_1, WAYBEL_0, TARSKI, PBOOLE, SETFAM_1, ORDINAL1, NAT_1, GLIB_002, XCMPLX_0; notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, SETFAM_1, DOMAIN_1, XCMPLX_0, ABIAN, XXREAL_0, RELAT_1, FUNCT_1, PBOOLE, FUNCT_2, FINSEQ_1, NAT_1, FUNCOP_1, GLIB_000, GLIB_001; constructors DOMAIN_1, CARD_FIL, GLIB_001, VALUED_1, XXREAL_2, WELLORD2, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XREAL_0, INT_1, CARD_1, GLIB_000, ABIAN, GLIB_001, FUNCT_2, PARTFUN1; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Definitions definition let G be _Graph; attr G is connected means :: GLIB_002:def 1 for u,v being Vertex of G holds ex W being Walk of G st W is_Walk_from u,v; end; definition let G be _Graph; attr G is acyclic means :: GLIB_002:def 2 not ex W being Walk of G st W is Cycle-like; end; definition let G be _Graph; attr G is Tree-like means :: GLIB_002:def 3 G is acyclic & G is connected; end; registration cluster trivial -> connected for _Graph; end; registration cluster trivial loopless -> Tree-like for _Graph; end; registration cluster acyclic -> simple for _Graph; end; registration cluster Tree-like -> acyclic connected for _Graph; end; registration cluster acyclic connected -> Tree-like for _Graph; end; registration let G be _Graph, v be Vertex of G; cluster -> Tree-like for inducedSubgraph of G,{v},{}; end; definition let G be _Graph, v be set; pred G is_DTree_rooted_at v means :: GLIB_002:def 4 G is Tree-like & for x being Vertex of G holds ex W being DWalk of G st W is_Walk_from v,x; end; registration cluster trivial finite Tree-like for _Graph; cluster non trivial finite Tree-like for _Graph; end; registration let G be _Graph; cluster trivial finite Tree-like for Subgraph of G; end; registration let G be acyclic _Graph; cluster -> acyclic for Subgraph of G; end; definition let G be _Graph, v be Vertex of G; func G.reachableFrom(v) -> non empty Subset of the_Vertices_of G means :: GLIB_002:def 5 for x being object holds x in it iff ex W being Walk of G st W is_Walk_from v,x; end; definition let G be _Graph, v be Vertex of G; func G.reachableDFrom(v) -> non empty Subset of the_Vertices_of G means :: GLIB_002:def 6 for x being object holds x in it iff ex W being DWalk of G st W is_Walk_from v,x; end; definition let G1 be _Graph, G2 be Subgraph of G1; attr G2 is Component-like means :: GLIB_002:def 7 G2 is connected & not ex G3 being connected Subgraph of G1 st G2 c< G3; end; registration let G be _Graph; cluster Component-like -> connected for Subgraph of G; end; registration let G be _Graph, v be Vertex of G; cluster -> Component-like for inducedSubgraph of G,G.reachableFrom(v); end; registration let G be _Graph; cluster Component-like for Subgraph of G; end; definition let G be _Graph; mode Component of G is Component-like Subgraph of G; end; definition let G be _Graph; func G.componentSet() -> non empty Subset-Family of the_Vertices_of G means :: GLIB_002:def 8 for x being set holds x in it iff ex v being Vertex of G st x = G .reachableFrom(v); end; registration let G be _Graph, X be Element of G.componentSet(); cluster -> Component-like for inducedSubgraph of G,X; end; definition let G be _Graph; func G.numComponents() -> Cardinal equals :: GLIB_002:def 9 card G.componentSet(); end; definition let G be finite _Graph; redefine func G.numComponents() -> non zero Element of NAT; end; definition let G be _Graph, v be Vertex of G; attr v is cut-vertex means :: GLIB_002:def 10 for G2 being removeVertex of G,v holds G .numComponents() in G2.numComponents(); end; definition let G be finite _Graph, v be Vertex of G; redefine attr v is cut-vertex means :: GLIB_002:def 11 for G2 being removeVertex of G,v holds G.numComponents() < G2.numComponents(); end; registration let G be non trivial finite connected _Graph; cluster non cut-vertex for Vertex of G; end; registration let G be non trivial finite Tree-like _Graph; cluster endvertex for Vertex of G; end; registration let G be non trivial finite Tree-like _Graph, v be endvertex Vertex of G; cluster -> Tree-like for removeVertex of G,v; end; definition let GF be Graph-yielding Function; attr GF is connected means :: GLIB_002:def 12 for x being object st x in dom GF ex G being _Graph st GF.x = G & G is connected; attr GF is acyclic means :: GLIB_002:def 13 for x being object st x in dom GF ex G being _Graph st GF.x = G & G is acyclic; attr GF is Tree-like means :: GLIB_002:def 14 for x being object st x in dom GF ex G being _Graph st GF.x = G & G is Tree-like; end; definition let GF be non empty Graph-yielding Function; redefine attr GF is connected means :: GLIB_002:def 15 for x being Element of dom GF holds GF.x is connected; redefine attr GF is acyclic means :: GLIB_002:def 16 for x being Element of dom GF holds GF.x is acyclic; redefine attr GF is Tree-like means :: GLIB_002:def 17 for x being Element of dom GF holds GF.x is Tree-like; end; definition let GSq be GraphSeq; redefine attr GSq is connected means :: GLIB_002:def 18 for n being Nat holds GSq.n is connected; redefine attr GSq is acyclic means :: GLIB_002:def 19 for n being Nat holds GSq.n is acyclic; redefine attr GSq is Tree-like means :: GLIB_002:def 20 for n being Nat holds GSq.n is Tree-like; end; registration cluster connected acyclic Tree-like non empty for Graph-yielding Function; end; registration cluster trivial -> connected for Graph-yielding Function; cluster trivial loopless -> Tree-like for Graph-yielding Function; cluster acyclic -> simple for Graph-yielding Function; cluster Tree-like -> acyclic connected for Graph-yielding Function; cluster acyclic connected -> Tree-like for Graph-yielding Function; end; registration cluster halting finite Tree-like for GraphSeq; end; registration let GF be connected non empty Graph-yielding Function; let x be Element of dom GF; cluster GF.x -> connected for _Graph; end; registration let GF be acyclic non empty Graph-yielding Function; let x be Element of dom GF; cluster GF.x -> acyclic for _Graph; end; registration let GF be Tree-like non empty Graph-yielding Function; let x be Element of dom GF; cluster GF.x -> Tree-like for _Graph; end; registration let GSq be connected GraphSeq, n be Nat; cluster GSq.n -> connected for _Graph; end; registration let GSq be acyclic GraphSeq, n be Nat; cluster GSq.n -> acyclic for _Graph; end; registration let GSq be Tree-like GraphSeq, n be Nat; cluster GSq.n -> Tree-likefor _Graph; end; begin :: Theorems reserve G,G1,G2 for _Graph; reserve e,x,y for set; reserve v,v1,v2 for Vertex of G; reserve W for Walk of G; ::\$CT theorem :: GLIB_002:2 for G being non trivial connected _Graph, v being Vertex of G holds not v is isolated; theorem :: GLIB_002:3 for G1 being non trivial _Graph, v being Vertex of G1, G2 being removeVertex of G1,v st G2 is connected & ex e being set st e in v.edgesInOut() & not e Joins v,v,G1 holds G1 is connected; theorem :: GLIB_002:4 for G1 being non trivial connected _Graph, v being Vertex of G1, G2 being removeVertex of G1,v st v is endvertex holds G2 is connected; theorem :: GLIB_002:5 for G1 being connected _Graph, W being Walk of G1, e being set, G2 being removeEdge of G1,e st W is Cycle-like & e in W.edges() holds G2 is connected; theorem :: GLIB_002:6 (ex v1 being Vertex of G st for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2) implies G is connected; theorem :: GLIB_002:7 for G being trivial _Graph holds G is connected; theorem :: GLIB_002:8 G1 == G2 & G1 is connected implies G2 is connected; theorem :: GLIB_002:9 v in G.reachableFrom(v); theorem :: GLIB_002:10 for e,x,y being object holds x in G.reachableFrom(v1) & e Joins x,y,G implies y in G.reachableFrom( v1); theorem :: GLIB_002:11 G.edgesBetween(G.reachableFrom(v)) = G.edgesInOut(G.reachableFrom(v)); theorem :: GLIB_002:12 v1 in G.reachableFrom(v2) implies G.reachableFrom(v1) = G .reachableFrom(v2); theorem :: GLIB_002:13 v in W.vertices() implies W.vertices() c= G.reachableFrom(v); theorem :: GLIB_002:14 for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds G2.reachableFrom(v2) c= G1.reachableFrom (v1); theorem :: GLIB_002:15 (ex v being Vertex of G st G.reachableFrom(v) = the_Vertices_of G) implies G is connected; theorem :: GLIB_002:16 G is connected implies for v being Vertex of G holds G.reachableFrom(v ) = the_Vertices_of G; theorem :: GLIB_002:17 for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds G1.reachableFrom(v1) = G2.reachableFrom(v2); theorem :: GLIB_002:18 v in G.reachableDFrom(v); theorem :: GLIB_002:19 x in G.reachableDFrom(v1) & e DJoins x,y,G implies y in G .reachableDFrom(v1) ; theorem :: GLIB_002:20 G.reachableDFrom(v) c= G.reachableFrom(v); theorem :: GLIB_002:21 for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds G2.reachableDFrom(v2) c= G1 .reachableDFrom(v1); theorem :: GLIB_002:22 for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds G1.reachableDFrom(v1) = G2.reachableDFrom(v2); theorem :: GLIB_002:23 for G1 being _Graph, G2 being connected Subgraph of G1 holds G2 is spanning implies G1 is connected; theorem :: GLIB_002:24 union G.componentSet() = the_Vertices_of G; theorem :: GLIB_002:25 G is connected iff G.componentSet() = {the_Vertices_of G}; theorem :: GLIB_002:26 G1 == G2 implies G1.componentSet() = G2.componentSet(); theorem :: GLIB_002:27 x in G.componentSet() implies x is non empty Subset of the_Vertices_of G; theorem :: GLIB_002:28 G is connected iff G.numComponents() = 1; theorem :: GLIB_002:29 G1 == G2 implies G1.numComponents() = G2.numComponents(); theorem :: GLIB_002:30 G is Component of G iff G is connected; theorem :: GLIB_002:31 for C being Component of G holds the_Edges_of C = G.edgesBetween( the_Vertices_of C); theorem :: GLIB_002:32 for C1,C2 being Component of G holds the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2; theorem :: GLIB_002:33 for C being Component of G, v being Vertex of G holds v in the_Vertices_of C iff the_Vertices_of C = G.reachableFrom(v); theorem :: GLIB_002:34 for C1,C2 being Component of G, v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds C1 == C2; theorem :: GLIB_002:35 for G being connected _Graph, v being Vertex of G holds v is non cut-vertex iff for G2 being removeVertex of G,v holds G2.numComponents() c= G .numComponents(); theorem :: GLIB_002:36 for G being connected _Graph, v being Vertex of G, G2 being removeVertex of G,v st not v is cut-vertex holds G2 is connected; theorem :: GLIB_002:37 for G being non trivial finite connected _Graph holds ex v1,v2 being Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex; theorem :: GLIB_002:38 v is cut-vertex implies G is non trivial; theorem :: GLIB_002:39 for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds v1 is cut-vertex implies v2 is cut-vertex; theorem :: GLIB_002:40 for G being finite connected _Graph holds G.order() <= G.size() + 1; theorem :: GLIB_002:41 for G being acyclic _Graph holds G is simple; theorem :: GLIB_002:42 for G being acyclic _Graph, W being Path of G, e being set st not e in W.edges() & e in W.last().edgesInOut() holds W.addEdge(e) is Path-like; theorem :: GLIB_002:43 for G being non trivial finite acyclic _Graph st the_Edges_of G <> {} holds ex v1,v2 being Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G.reachableFrom(v1); theorem :: GLIB_002:44 G1 == G2 & G1 is acyclic implies G2 is acyclic; theorem :: GLIB_002:45 for G being non trivial finite Tree-like _Graph holds ex v1,v2 being Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex; theorem :: GLIB_002:46 for G being finite _Graph holds G is Tree-like iff G is acyclic & G.order() = G.size() + 1; theorem :: GLIB_002:47 for G being finite _Graph holds G is Tree-like iff G is connected & G .order() = G.size() + 1; theorem :: GLIB_002:48 G1 == G2 & G1 is Tree-like implies G2 is Tree-like; theorem :: GLIB_002:49 G is_DTree_rooted_at x implies x is Vertex of G; theorem :: GLIB_002:50 G1 == G2 & G1 is_DTree_rooted_at x implies G2 is_DTree_rooted_at x;