:: Trees: Connected, Acyclic Graphs :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2019 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; definitions TARSKI; equalities FUNCOP_1, ORDINAL1, CARD_1; expansions TARSKI; theorems CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, GLIB_000, GLIB_001, ABIAN, INT_1, JORDAN12, NAT_1, ORDINAL1, PENCIL_1, TARSKI, XBOOLE_0, XCMPLX_1, ZFMISC_1, XREAL_1, XXREAL_0, RELSET_1, PARTFUN1; schemes NAT_1, SUBSET_1, GLIB_000; begin :: Definitions definition let G be _Graph; attr G is connected means :Def1: 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 :Def2: not ex W being Walk of G st W is Cycle-like; end; definition let G be _Graph; attr G is Tree-like means G is acyclic & G is connected; end; registration cluster trivial -> connected for _Graph; coherence proof let G be _Graph; assume G is trivial; then consider x being Vertex of G such that A1: the_Vertices_of G = {x} by GLIB_000:22; now set W = G.walkOf(x); let u,v be Vertex of G; u = x & v = x by A1,TARSKI:def 1; then W is_Walk_from u,v by GLIB_001:13; hence ex W being Walk of G st W is_Walk_from u,v; end; hence thesis; end; end; registration cluster trivial loopless -> Tree-like for _Graph; coherence proof let G be _Graph; assume that A1: G is trivial and A2: G is loopless; now given W being Walk of G such that A3: W is Cycle-like; W.edges() <> {} by A3,GLIB_001:136; then ex e being object st e in W.edges() by XBOOLE_0:def 1; hence contradiction by A1,A2,GLIB_000:23; end; then A4: G is acyclic; reconsider G9=G as trivial _Graph by A1; G9 is connected; hence thesis by A4; end; end; registration cluster acyclic -> simple for _Graph; coherence proof let G be _Graph; assume A1: not ex W being Walk of G st W is Cycle-like; now given e being object such that A2: e in the_Edges_of G and A3: (the_Source_of G).e = (the_Target_of G).e; set v1 = (the_Source_of G).e; reconsider v1 as Vertex of G by A2,FUNCT_2:5; set W = G.walkOf(v1,e,v1); e Joins v1,v1,G by A2,A3,GLIB_000:def 13; then len W = 3 by GLIB_001:14; then W is non trivial by GLIB_001:125; then W is Cycle-like by GLIB_001:def 31; hence contradiction by A1; end; then A4: G is loopless by GLIB_000:def 18; now let e1,e2,v1,v2 be object; assume that A5: e1 Joins v1,v2,G and A6: e2 Joins v1,v2,G; A7: e2 Joins v2,v1,G by A6,GLIB_000:14; A8: v1 <> v2 by A4,A5,GLIB_000:18; now set W1 = G.walkOf(v1,e1,v2), W = W1.addEdge(e2); assume A9: e1 <> e2; reconsider W1 as Path of G; A10: W1.last() = v2 by A5,GLIB_001:15; then A11: W.last() = v1 by A7,GLIB_001:63; A12: len W1 = 3 by A5,GLIB_001:14; A13: now let n be odd Element of NAT; assume that A14: 1 < n and A15: n <= len W1; 1+1 <= n by A14,NAT_1:13; then 2*1 < n by XXREAL_0:1; then 2*1+1 <= n by NAT_1:13; then A16: n = 3 by A12,A15,XXREAL_0:1; W1 = <*v1,e1,v2*> by A5,GLIB_001:def 5; hence W1.n <> v1 by A8,A16,FINSEQ_1:45; end; W1.first() = v1 & W1.last() = v2 by A5,GLIB_001:15; then A17: W1 is open by A8,GLIB_001:def 24; W1.first() = v1 by A5,GLIB_001:15; then W.first() = v1 by A7,A10,GLIB_001:63; then A18: W is closed by A11,GLIB_001:def 24; A19: e2 Joins W1.last(), v1, G by A5,A7,GLIB_001:15; then A20: W is non trivial by GLIB_001:132; W1.edges() = {e1} by A5,GLIB_001:108; then not e2 in W1.edges() by A9,TARSKI:def 1; hence W is Path-like by A19,A17,A13,GLIB_001:150; then W is Cycle-like by A18,A20,GLIB_001:def 31; hence contradiction by A1; end; hence e1 = e2; end; then G is non-multi by GLIB_000:def 20; hence thesis by A4; end; end; registration cluster Tree-like -> acyclic connected for _Graph; coherence; end; registration cluster acyclic connected -> Tree-like for _Graph; coherence; end; registration let G be _Graph, v be Vertex of G; cluster -> Tree-like for inducedSubgraph of G,{v},{}; coherence; end; definition let G be _Graph, v be set; pred G is_DTree_rooted_at v means 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; existence proof set V = {1}, E = {}; reconsider S = {} as Function of E,V by RELSET_1:12; set G = createGraph(V,E,S,S); take G; thus thesis; end; cluster non trivial finite Tree-like for _Graph; existence proof set V = {0,1}, E = {0}, S = 0 .--> 0, T = 0 .--> 1; A1: dom T = E; A2: now let x be object; assume x in E; then x = 0 by TARSKI:def 1; then T.x = 1 by FUNCOP_1:72; hence T.x in V by TARSKI:def 2; end; A3: now let x be object; assume x in E; S.x = 0; hence S.x in V by TARSKI:def 2; end; reconsider T as Function of E,V by A1,A2,FUNCT_2:3; dom S = E; then reconsider S as Function of E,V by A3,FUNCT_2:3; set G = createGraph(V,E,S,T); A4: the_Edges_of G = E by GLIB_000:6; the_Target_of G = T by GLIB_000:6; then A5: (the_Target_of G).0 = 1 by FUNCOP_1:72; the_Source_of G = S by GLIB_000:6; then A6: (the_Source_of G).0 = 0; now given W being Walk of G such that A7: W is Cycle-like; now per cases; suppose A8: len W = 3; set e = W.(1+1), v1 = W.1, v2 = W.(1+2); A9: W.(1+1) Joins W.1, W.(1+2), G by A8,GLIB_001:def 3,JORDAN12:2; v1 = v2 by A7,A8,GLIB_001:118; then A10: (the_Source_of G).e = v1 & (the_Target_of G).e = v1 or ( the_Source_of G).e = v1 & (the_Target_of G).e = v1 by A9,GLIB_000:def 13; e in the_Edges_of G by A9,GLIB_000:def 13; then v1 = 0 & v1 = 1 or v1 = 1 & v1 = 0 by A4,A6,A5,A10,TARSKI:def 1; hence contradiction; end; suppose A11: len W <> 3; A12: 3 <= len W by A7,GLIB_001:125; then 3-1 <= len W - 0 by XREAL_1:13; then 2*1 in dom W by FINSEQ_3:25; then W.(2*1) in {0} by A4,GLIB_001:8; then A13: W.(2*1) = 0 by TARSKI:def 1; 3 < len W by A11,A12,XXREAL_0:1; then A14: 3+1 <= len W by NAT_1:13; then 2*2 in dom W by FINSEQ_3:25; then W.(2*2) in {0} by A4,GLIB_001:8; then W.(2*2) = 0 by TARSKI:def 1; hence contradiction by A7,A14,A13,GLIB_001:138; end; end; hence contradiction; end; then A15: G is acyclic; set W1 = G.walkOf(0,0,1), W2 = W1.reverse(); take G; A16: the_Vertices_of G = V by GLIB_000:6; then reconsider a0 = 0, a1 = 1 as Vertex of G by TARSKI:def 2; now assume card (the_Vertices_of G) = 1; then ex x being object st the_Vertices_of G = {x} by CARD_2:42; hence contradiction by A16,ZFMISC_1:5; end; hence G is non trivial & G is finite by GLIB_000:def 19; 0 in the_Edges_of G by A4,TARSKI:def 1; then 0 Joins 0,1, G by A6,A5,GLIB_000:def 13; then A17: W1 is_Walk_from 0,1 by GLIB_001:15; then A18: W2 is_Walk_from 1,0 by GLIB_001:23; now let u,v be Vertex of G; now per cases by A16,TARSKI:def 2; suppose u = 0 & v = 0; then G.walkOf(a0) is_Walk_from u,v by GLIB_001:13; hence ex W being Walk of G st W is_Walk_from u,v; end; suppose u = 0 & v = 1; hence ex W being Walk of G st W is_Walk_from u,v by A17; end; suppose u = 1 & v = 0; hence ex W being Walk of G st W is_Walk_from u,v by A18; end; suppose u = 1 & v = 1; then G.walkOf(a1) is_Walk_from u,v by GLIB_001:13; hence ex W being Walk of G st W is_Walk_from u,v; end; end; hence ex W being Walk of G st W is_Walk_from u,v; end; then G is connected; hence thesis by A15; end; end; registration let G be _Graph; cluster trivial finite Tree-like for Subgraph of G; existence proof set IT = the finite trivial simple Subgraph of G; take IT; thus thesis; end; end; registration let G be acyclic _Graph; cluster -> acyclic for Subgraph of G; coherence proof let G2 be Subgraph of G; now given W2 being Walk of G2 such that A1: W2 is Cycle-like; reconsider W = W2 as Walk of G by GLIB_001:167; A2: W is Path-like by A1,GLIB_001:176; W is closed & W is non trivial by A1,GLIB_001:176; then W is Cycle-like by A2,GLIB_001:def 31; hence contradiction by Def2; end; hence thesis; end; end; definition let G be _Graph, v be Vertex of G; func G.reachableFrom(v) -> non empty Subset of the_Vertices_of G means :Def5: for x being object holds x in it iff ex W being Walk of G st W is_Walk_from v,x; existence proof defpred P[set] means ex W being Walk of G st W is_Walk_from v,$1; consider IT being Subset of the_Vertices_of G such that A1: for x being set holds x in IT iff x in the_Vertices_of G & P[x] from SUBSET_1:sch 1; G.walkOf(v) is_Walk_from v,v by GLIB_001:13; then reconsider IT as non empty Subset of the_Vertices_of G by A1; take IT; let x being object; thus x in IT implies ex W being Walk of G st W is_Walk_from v,x by A1; assume A2: ex W being Walk of G st W is_Walk_from v, x; then x is Vertex of G by GLIB_001:18; hence thesis by A1,A2; end; uniqueness proof let IT1, IT2 be non empty Subset of the_Vertices_of G such that A3: for x being object holds x in IT1 iff ex W being Walk of G st W is_Walk_from v,x and A4: for x being object holds x in IT2 iff ex W being Walk of G st W is_Walk_from v,x; now let x be object; hereby assume x in IT1; then ex W being Walk of G st W is_Walk_from v, x by A3; hence x in IT2 by A4; end; assume x in IT2; then ex W being Walk of G st W is_Walk_from v, x by A4; hence x in IT1 by A3; end; hence thesis by TARSKI:2; end; end; definition let G be _Graph, v be Vertex of G; func G.reachableDFrom(v) -> non empty Subset of the_Vertices_of G means :Def6: for x being object holds x in it iff ex W being DWalk of G st W is_Walk_from v,x; existence proof set W = G.walkOf(v); defpred P[set] means ex W being directed Walk of G st W is_Walk_from v,$1; consider IT being Subset of the_Vertices_of G such that A1: for x being set holds x in IT iff x in the_Vertices_of G & P[x] from SUBSET_1:sch 1; W is_Walk_from v,v by GLIB_001:13; then reconsider IT as non empty Subset of the_Vertices_of G by A1; take IT; let x be object; thus x in IT implies ex W being directed Walk of G st W is_Walk_from v,x by A1; given W being directed Walk of G such that A2: W is_Walk_from v, x; x is Vertex of G by A2,GLIB_001:18; hence thesis by A1,A2; end; uniqueness proof let IT1, IT2 be non empty Subset of the_Vertices_of G such that A3: for x being object holds x in IT1 iff ex W being directed Walk of G st W is_Walk_from v,x and A4: for x being object holds x in IT2 iff ex W being directed Walk of G st W is_Walk_from v,x; now let x be object; hereby assume x in IT1; then ex W being directed Walk of G st W is_Walk_from v, x by A3; hence x in IT2 by A4; end; assume x in IT2; then ex W being directed Walk of G st W is_Walk_from v, x by A4; hence x in IT1 by A3; end; hence thesis by TARSKI:2; end; end; Lm1: for G being _Graph, v being Vertex of G holds v in G.reachableFrom(v) proof let G be _Graph, v be Vertex of G; G.walkOf(v) is_Walk_from v,v by GLIB_001:13; hence thesis by Def5; end; Lm2: for G being _Graph, v1 being Vertex of G, e,x,y being object holds x in G .reachableFrom(v1) & e Joins x,y,G implies y in G.reachableFrom(v1) proof let G be _Graph, v1 be Vertex of G, e,x,y be object; set RFV = G.reachableFrom(v1); assume that A1: x in RFV and A2: e Joins x,y,G; consider W being Walk of G such that A3: W is_Walk_from v1,x by A1,Def5; W.addEdge(e) is_Walk_from v1,y by A2,A3,GLIB_001:66; hence thesis by Def5; end; Lm3: for G being _Graph, v1,v2 being Vertex of G holds v1 in G.reachableFrom( v2) implies G.reachableFrom(v1) = G.reachableFrom(v2) proof let G be _Graph, v1,v2 be Vertex of G; assume v1 in G.reachableFrom(v2); then consider WA being Walk of G such that A1: WA is_Walk_from v2,v1 by Def5; A2: WA.reverse() is_Walk_from v1,v2 by A1,GLIB_001:23; now let x be object; hereby assume x in G.reachableFrom(v1); then consider WB being Walk of G such that A3: WB is_Walk_from v1,x by Def5; WA.append(WB) is_Walk_from v2,x by A1,A3,GLIB_001:31; hence x in G.reachableFrom(v2) by Def5; end; assume x in G.reachableFrom(v2); then consider WB being Walk of G such that A4: WB is_Walk_from v2,x by Def5; WA.reverse().append(WB) is_Walk_from v1,x by A2,A4,GLIB_001:31; hence x in G.reachableFrom(v1) by Def5; end; hence thesis by TARSKI:2; end; Lm4: for G being _Graph, W being Walk of G, v being Vertex of G holds v in W .vertices() implies W.vertices() c= G.reachableFrom(v) proof let G be _Graph, W be Walk of G, v be Vertex of G; assume v in W.vertices(); then consider m being odd Element of NAT such that A1: m <= len W and A2: W.m = v by GLIB_001:87; let x be object; assume x in W.vertices(); then consider n being odd Element of NAT such that A3: n <= len W and A4: W.n = x by GLIB_001:87; now per cases; suppose m <= n; then W.cut(m,n) is_Walk_from v,x by A2,A3,A4,GLIB_001:37; hence ex W2 being Walk of G st W2 is_Walk_from v,x; end; suppose m > n; then W.cut(n,m) is_Walk_from x,v by A1,A2,A4,GLIB_001:37; then W.cut(n,m).reverse() is_Walk_from v,x by GLIB_001:23; hence ex W2 being Walk of G st W2 is_Walk_from v,x; end; end; hence thesis by Def5; end; definition let G1 be _Graph, G2 be Subgraph of G1; attr G2 is Component-like means :Def7: 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; coherence; end; registration let G be _Graph, v be Vertex of G; cluster -> Component-like for inducedSubgraph of G,G.reachableFrom(v); coherence proof let G2 be inducedSubgraph of G,G.reachableFrom(v); A1: the_Vertices_of G2 = G.reachableFrom(v) by GLIB_000:def 37; A2: the_Edges_of G2 = G.edgesBetween(G.reachableFrom(v)) by GLIB_000:def 37; A3: now A4: v in the_Vertices_of G2 by A1,Lm1; given G3 being connected Subgraph of G such that A5: G2 c< G3; G2 c= G3 by A5,GLIB_000:def 36; then A6: G2 is Subgraph of G3 by GLIB_000:def 35; then A7: the_Vertices_of G2 c= the_Vertices_of G3 by GLIB_000:def 32; A8: now given x being object such that A9: x in the_Vertices_of G3 and A10: not x in the_Vertices_of G2; consider W being Walk of G3 such that A11: W is_Walk_from v,x by A4,A7,A9,Def1; reconsider W as Walk of G by GLIB_001:167; W is_Walk_from v,x by A11,GLIB_001:19; hence contradiction by A1,A10,Def5; end; A12: the_Vertices_of G2 c= the_Vertices_of G3 by A6,GLIB_000:def 32; now per cases by A5,GLIB_000:99; suppose ex x being object st x in the_Vertices_of G3 & not x in the_Vertices_of G2; hence contradiction by A8; end; suppose ex e being object st e in the_Edges_of G3 & not e in the_Edges_of G2; then consider e being set such that A13: e in the_Edges_of G3 and A14: not e in the_Edges_of G2; set v1 = (the_Source_of G3).e, v2 = (the_Target_of G3).e; A15: e Joins v1,v2,G3 by A13,GLIB_000:def 13; then A16: e Joins v1,v2,G by GLIB_000:72; now per cases; suppose the_Vertices_of G3 = the_Vertices_of G2; then reconsider v1,v2 as Vertex of G2 by A15,GLIB_000:13; v1 in G.reachableFrom(v) & v2 in G.reachableFrom(v) by A1; hence contradiction by A2,A14,A16,GLIB_000:32; end; suppose the_Vertices_of G3 <> the_Vertices_of G2; then the_Vertices_of G2 c< the_Vertices_of G3 by A12, XBOOLE_0:def 8; hence contradiction by A8,XBOOLE_0:6; end; end; hence contradiction; end; end; hence contradiction; end; now let x,y be Vertex of G2; consider W1R being Walk of G such that A17: W1R is_Walk_from v,x by A1,Def5; consider W2 being Walk of G such that A18: W2 is_Walk_from v,y by A1,Def5; set W1 = W1R.reverse(), W = W1.append(W2); A19: W1 is_Walk_from x,v by A17,GLIB_001:23; then A20: W is_Walk_from x,y by A18,GLIB_001:31; A21: W1.last() = v by A19,GLIB_001:def 23; then A22: v in W1.vertices() by GLIB_001:88; A23: W.edges() c= G.edgesBetween(W.vertices()) by GLIB_001:109; W2.first() = v by A18,GLIB_001:def 23; then W.vertices() = W1.vertices() \/ W2.vertices() by A21,GLIB_001:93; then A24: v in W.vertices() by A22,XBOOLE_0:def 3; then G.edgesBetween(W.vertices()) c= G.edgesBetween(the_Vertices_of G2) by A1,Lm4,GLIB_000:36; then W.edges() c= G.edgesBetween(the_Vertices_of G2) by A23; then reconsider W as Walk of G2 by A1,A2,A24,Lm4,GLIB_001:170; take W; thus W is_Walk_from x,y by A20,GLIB_001:19; end; then G2 is connected; hence thesis by A3; end; end; registration let G be _Graph; cluster Component-like for Subgraph of G; existence proof set v = the Vertex of G; set IT = the inducedSubgraph of G,G.reachableFrom(v); take IT; thus thesis; end; 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 :Def8: for x being set holds x in it iff ex v being Vertex of G st x = G .reachableFrom(v); existence proof set v = the Vertex of G; defpred P[set] means ex v being Vertex of G st $1 = G.reachableFrom(v); consider IT being Subset-Family of the_Vertices_of G such that A1: for x being set holds x in IT iff x in bool the_Vertices_of G & P[ x] from SUBSET_1:sch 1; set x = G.reachableFrom(v); x in IT by A1; then reconsider IT as non empty Subset-Family of the_Vertices_of G; take IT; thus thesis by A1; end; uniqueness proof defpred P[object] means ex v being Vertex of G st $1 = G.reachableFrom(v); let IT1,IT2 be non empty Subset-Family of the_Vertices_of G such that A2: for x being set holds x in IT1 iff P[x] and A3: for x being set holds x in IT2 iff P[x]; now let x be object; x in IT1 iff P[x] by A2; hence x in IT1 iff x in IT2 by A3; end; hence thesis by TARSKI:2; end; end; registration let G be _Graph, X be Element of G.componentSet(); cluster -> Component-like for inducedSubgraph of G,X; coherence proof let G2 be inducedSubgraph of G,X; ex v being Vertex of G st X = G.reachableFrom(v) by Def8; hence thesis; end; end; definition let G be _Graph; func G.numComponents() -> Cardinal equals card G.componentSet(); coherence; end; definition let G be finite _Graph; redefine func G.numComponents() -> non zero Element of NAT; coherence proof G.numComponents() = card G.componentSet(); hence thesis; end; end; definition let G be _Graph, v be Vertex of G; attr v is cut-vertex means 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 for G2 being removeVertex of G,v holds G.numComponents() < G2.numComponents(); compatibility proof hereby assume A1: v is cut-vertex; let G2 be removeVertex of G,v; card Segm G.numComponents() in card Segm G2.numComponents() by A1; hence G.numComponents() < G2.numComponents() by NAT_1:41; end; assume A2: for G2 being removeVertex of G,v holds G.numComponents() < G2 .numComponents(); now let G2 be removeVertex of G,v; G.numComponents() < G2.numComponents() by A2; then card Segm G.numComponents() in card Segm G2.numComponents() by NAT_1:41; hence G.numComponents() in G2.numComponents(); end; hence thesis; end; end; Lm5: 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 proof let G1 be non trivial connected _Graph, v being Vertex of G1, G2 be removeVertex of G1,v; set VG = the_Vertices_of G1, VG2 = the_Vertices_of G2; assume A1: v is endvertex; then consider ev being object such that A2: v.edgesInOut() = {ev} and not ev Joins v, v,G1 by GLIB_000:def 51; now let v19,v29 be Vertex of G2; reconsider v1=v19, v2=v29 as Vertex of G1 by GLIB_000:42; consider W being Walk of G1 such that A3: W is_Walk_from v1,v2 by Def1; set T = the Trail of W; A4: T is_Walk_from v1, v2 by A3,GLIB_001:160; then A5: T.(len T) = v2 by GLIB_001:17; v19 in VG2; then v19 in VG \ {v} by GLIB_000:47; then A6: not v1 in {v} by XBOOLE_0:def 5; v29 in VG2; then v29 in VG \ {v} by GLIB_000:47; then not v2 in {v} by XBOOLE_0:def 5; then A7: v2 <> v by TARSKI:def 1; A8: T.1 = v1 by A4,GLIB_001:17; now let e be object; assume A9: e in T.edges(); then consider n being even Element of NAT such that A10: 1 <= n and A11: n <= len T and A12: T.n = e by GLIB_001:99; n in dom T by A10,A11,FINSEQ_3:25; then consider n1 being odd Element of NAT such that A13: n1 = n-1 and A14: n-1 in dom T and A15: n+1 in dom T and A16: T.n Joins T.(n1), T.(n+1),G1 by GLIB_001:9; A17: n+1 <= len T by A15,FINSEQ_3:25; A18: n1 <= len T by A13,A14,FINSEQ_3:25; now assume A19: e in v.edgesInOut(); then A20: e = ev by A2,TARSKI:def 1; now per cases by A12,A16,A19,GLIB_000:65; suppose A21: T.(n1) = v; reconsider n2 = n1 - 1 as even Element of NAT by ABIAN:12,INT_1:5; A22: 1 <= n1 by ABIAN:12; n1 <> 1 by A6,A8,A21,TARSKI:def 1; then A23: 1 < n1 by A22,XXREAL_0:1; then 1+1 <= n1 by NAT_1:13; then A24: 1+1-1 <= n2 by XREAL_1:13; T.vertexAt(n1) = v by A18,A21,GLIB_001:def 8; then T.n2 in v.edgesInOut() by A18,A23,GLIB_001:11; then A25: T.n = T.n2 by A2,A12,A20,TARSKI:def 1; n - 1 < n - 0 by XREAL_1:15; then n1 - 1 < n - 0 by A13,XREAL_1:14; hence contradiction by A11,A25,A24,GLIB_001:138; end; suppose A26: T.(n+1) = v; then A27: n+1 < len T by A7,A5,A17,XXREAL_0:1; T.vertexAt(n+1) = v by A17,A26,GLIB_001:def 8; then T.(n+1+1) in v.edgesInOut() by A27,GLIB_001:10; then A28: T.n = T.(n+1+1) by A2,A12,A20,TARSKI:def 1; n + 0 < n+(1+1) & n+1+1 <= len T by A27,NAT_1:13,XREAL_1:8; hence contradiction by A10,A28,GLIB_001:138; end; end; hence contradiction; end; then e in (the_Edges_of G1) \ v.edgesInOut() by A9,XBOOLE_0:def 5; then e in (the_Edges_of G1) \ G1.edgesInOut({v}) by GLIB_000:def 40; then e in G1.edgesBetween( the_Vertices_of G1 \ {v}) by GLIB_000:35; hence e in the_Edges_of G2 by GLIB_000:47; end; then A29: T.edges() c= the_Edges_of G2; A30: v1 <> v by A6,TARSKI:def 1; now let x be object; assume A31: x in T.vertices(); now assume x = v; then v = T.first() or v = T.last() by A1,A31,GLIB_001:143; hence contradiction by A30,A7,A4,GLIB_001:def 23; end; then not x in {v} by TARSKI:def 1; then x in VG \ {v} by A31,XBOOLE_0:def 5; hence x in VG2 by GLIB_000:47; end; then T.vertices() c= VG2; then reconsider W9=T as Walk of G2 by A29,GLIB_001:170; W9 is_Walk_from v19,v29 by A4,GLIB_001:19; hence ex W being Walk of G2 st W is_Walk_from v19,v29; end; hence thesis; end; Lm6: for G being _Graph holds (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 proof let G be _Graph; given v1 being Vertex of G such that A1: for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1, v2; now let x,y be Vertex of G; consider W1 being Walk of G such that A2: W1 is_Walk_from v1,x by A1; consider W2 being Walk of G such that A3: W2 is_Walk_from v1,y by A1; W1.reverse() is_Walk_from x,v1 by A2,GLIB_001:23; then W1.reverse().append(W2) is_Walk_from x,y by A3,GLIB_001:31; hence ex W being Walk of G st W is_Walk_from x,y; end; hence thesis; end; Lm7: for G being _Graph holds (ex v being Vertex of G st G.reachableFrom(v) = the_Vertices_of G) implies G is connected proof let G be _Graph; assume ex v being Vertex of G st G.reachableFrom(v)=the_Vertices_of G; then consider v being Vertex of G such that A1: G.reachableFrom(v) = the_Vertices_of G; now let x,y be Vertex of G; consider W1 being Walk of G such that A2: W1 is_Walk_from v,x by A1,Def5; consider W2 being Walk of G such that A3: W2 is_Walk_from v,y by A1,Def5; W1.reverse() is_Walk_from x,v by A2,GLIB_001:23; then W1.reverse().append(W2) is_Walk_from x,y by A3,GLIB_001:31; hence ex W being Walk of G st W is_Walk_from x,y; end; hence thesis; end; Lm8: for G being _Graph holds G is connected implies for v being Vertex of G holds G.reachableFrom(v) = the_Vertices_of G proof let G be _Graph; assume A1: G is connected; let v be Vertex of G; now let x be object; thus x in G.reachableFrom(v) implies x in the_Vertices_of G; assume x in the_Vertices_of G; then ex W being Walk of G st W is_Walk_from v,x by A1; hence x in G.reachableFrom(v) by Def5; end; hence thesis by TARSKI:2; end; Lm9: for G1,G2 being _Graph,v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds G1.reachableFrom(v1) = G2.reachableFrom(v2) proof let G1,G2 be _Graph, v1 be Vertex of G1, v2 be Vertex of G2; assume that A1: G1 == G2 and A2: v1 = v2; now let x be object; hereby assume x in G1.reachableFrom(v1); then consider W being Walk of G1 such that A3: W is_Walk_from v2,x by A2,Def5; reconsider W2 = W as Walk of G2 by A1,GLIB_001:179; W2 is_Walk_from v2,x by A3,GLIB_001:19; hence x in G2.reachableFrom(v2) by Def5; end; assume x in G2.reachableFrom(v2); then consider W being Walk of G2 such that A4: W is_Walk_from v1,x by A2,Def5; reconsider W2 = W as Walk of G1 by A1,GLIB_001:179; W2 is_Walk_from v1,x by A4,GLIB_001:19; hence x in G1.reachableFrom(v1) by Def5; end; hence thesis by TARSKI:2; end; Lm10: for G1 being _Graph, G2 being connected Subgraph of G1 holds G2 is spanning implies G1 is connected proof let G1 be _Graph, G2 be connected Subgraph of G1; assume A1: G2 is spanning; now let u9,v9 be Vertex of G1; reconsider u=u9, v=v9 as Vertex of G2 by A1,GLIB_000:def 33; consider W being Walk of G2 such that A2: W is_Walk_from u,v by Def1; reconsider W as Walk of G1 by GLIB_001:167; take W; thus W is_Walk_from u9,v9 by A2,GLIB_001:19; end; hence thesis; end; Lm11: for G being _Graph holds G is connected iff G.componentSet() = { the_Vertices_of G} proof let G be _Graph; hereby assume A1: G is connected; now set v = the Vertex of G; let x be object; hereby assume x in G.componentSet(); then ex v being Vertex of G st x = G.reachableFrom(v) by Def8; then x = the_Vertices_of G by A1,Lm8; hence x in {the_Vertices_of G} by TARSKI:def 1; end; assume x in {the_Vertices_of G}; then A2: x = the_Vertices_of G by TARSKI:def 1; G.reachableFrom(v) = the_Vertices_of G by A1,Lm8; hence x in G.componentSet() by A2,Def8; end; hence G.componentSet() = {the_Vertices_of G} by TARSKI:2; end; assume G.componentSet() = {the_Vertices_of G}; then the_Vertices_of G in G.componentSet() by TARSKI:def 1; then ex v being Vertex of G st G.reachableFrom(v) = the_Vertices_of G by Def8 ; hence thesis by Lm7; end; Lm12: for G1,G2 being _Graph holds G1 == G2 implies G1.componentSet() = G2 .componentSet() proof let G1,G2 be _Graph; assume A1: G1 == G2; now let x be object; hereby assume x in G1.componentSet(); then consider v1 being Vertex of G1 such that A2: x = G1.reachableFrom(v1) by Def8; reconsider v2 = v1 as Vertex of G2 by A1,GLIB_000:def 34; x = G2.reachableFrom(v2) by A1,A2,Lm9; hence x in G2.componentSet() by Def8; end; assume x in G2.componentSet(); then consider v2 being Vertex of G2 such that A3: x = G2.reachableFrom(v2) by Def8; reconsider v1 = v2 as Vertex of G1 by A1,GLIB_000:def 34; x = G1.reachableFrom(v1) by A1,A3,Lm9; hence x in G1.componentSet() by Def8; end; hence thesis by TARSKI:2; end; Lm13: for G being _Graph, x being set holds x in G.componentSet() implies x is non empty Subset of the_Vertices_of G proof let G be _Graph, x be set; assume x in G.componentSet(); then ex v being Vertex of G st x = G.reachableFrom(v) by Def8; hence thesis; end; Lm14: for G being _Graph, C being Component of G holds the_Edges_of C = G .edgesBetween(the_Vertices_of C) proof let G be _Graph, C be Component of G; reconsider VC = the_Vertices_of C as Subset of the_Vertices_of G; set EB = G.edgesBetween(VC); C.edgesBetween(the_Vertices_of C) c= EB by GLIB_000:76; then A1: the_Edges_of C c= EB by GLIB_000:34; now let e be object; thus e in the_Edges_of C implies e in EB by A1; assume A2: e in EB; now set GX = the inducedSubgraph of G,VC,EB; assume A3: not e in the_Edges_of C; A4: the_Edges_of GX = EB by GLIB_000:def 37; the_Vertices_of GX = VC by GLIB_000:def 37; then A5: C is spanning Subgraph of GX by A1,A4,GLIB_000:44,def 33; then GX is connected by Lm10; then not C c< GX by Def7; then GX == C or not C c= GX by GLIB_000:def 36; hence contradiction by A2,A3,A4,A5,GLIB_000:def 34,def 35; end; hence e in the_Edges_of C; end; hence thesis by TARSKI:2; end; Lm15: for G being _Graph, C1,C2 being Component of G holds the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 proof let G be _Graph, C1,C2 be Component of G; hereby assume A1: the_Vertices_of C1 = the_Vertices_of C2; then the_Edges_of C1 = G.edgesBetween(the_Vertices_of C2) by Lm14 .= the_Edges_of C2 by Lm14; hence C1 == C2 by A1,GLIB_000:86; end; assume C1 == C2; hence thesis by GLIB_000:def 34; end; Lm16: for G being _Graph, 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) proof let G be _Graph, C be Component of G, v be Vertex of G; hereby assume A1: v in the_Vertices_of C; now let x be object; hereby assume x in the_Vertices_of C; then reconsider x9=x as Vertex of C; consider W being Walk of C such that A2: W is_Walk_from v,x9 by A1,Def1; reconsider W as Walk of G by GLIB_001:167; W is_Walk_from v,x by A2,GLIB_001:19; hence x in G.reachableFrom(v) by Def5; end; assume A3: x in G.reachableFrom(v); then reconsider x9=x as Vertex of G; A4: G.reachableFrom(x9) = G.reachableFrom(v) by A3,Lm3; set CX = the inducedSubgraph of G,G.reachableFrom(x9); not C c< CX by Def7; then A5: C == CX or not C c= CX by GLIB_000:def 36; A6: the_Edges_of CX = G.edgesBetween(G.reachableFrom(x9)) by GLIB_000:def 37; now let e be object; set v1 = (the_Source_of C).e, v2 = (the_Target_of C).e; assume A7: e in the_Edges_of C; then reconsider v1,v2 as Vertex of C by FUNCT_2:5; e Joins v1,v2,C by A7,GLIB_000:def 13; then A8: e Joins v1,v2,G by GLIB_000:72; consider W1 being Walk of C such that A9: W1 is_Walk_from v,v1 by A1,Def1; reconsider W1 as Walk of G by GLIB_001:167; consider W2 being Walk of C such that A10: W2 is_Walk_from v,v2 by A1,Def1; reconsider W2 as Walk of G by GLIB_001:167; W2 is_Walk_from v,v2 by A10,GLIB_001:19; then A11: v2 in G.reachableFrom(x9) by A4,Def5; W1 is_Walk_from v,v1 by A9,GLIB_001:19; then v1 in G.reachableFrom(x9) by A4,Def5; hence e in the_Edges_of CX by A6,A8,A11,GLIB_000:32; end; then A12: the_Edges_of C c= the_Edges_of CX; A13: the_Vertices_of CX = G.reachableFrom(x9) by GLIB_000:def 37; now let z be object; assume z in the_Vertices_of C; then consider W being Walk of C such that A14: W is_Walk_from v,z by A1,Def1; reconsider W as Walk of G by GLIB_001:167; W is_Walk_from v,z by A14,GLIB_001:19; hence z in the_Vertices_of CX by A13,A4,Def5; end; then the_Vertices_of C c= the_Vertices_of CX; then A15: C is Subgraph of CX by A12,GLIB_000:44; x in the_Vertices_of CX by A13,Lm1; hence x in the_Vertices_of C by A5,A15,GLIB_000:def 34,def 35; end; hence the_Vertices_of C = G.reachableFrom(v) by TARSKI:2; end; assume the_Vertices_of C = G.reachableFrom(v); hence thesis by Lm1; end; Lm17: for G being _Graph, 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 proof let G be _Graph, C1,C2 be Component of G, v be set; assume that A1: v in the_Vertices_of C1 and A2: v in the_Vertices_of C2; reconsider v9 = v as Vertex of G by A1; the_Vertices_of C1 = G.reachableFrom(v9) & the_Vertices_of C2 = G .reachableFrom(v9) by A1,A2,Lm16; hence thesis by Lm15; end; Lm18: for G being _Graph holds G is connected iff G.numComponents() = 1 proof let G be _Graph; hereby assume G is connected; then G.componentSet() = {the_Vertices_of G} by Lm11; hence G.numComponents() = 1 by CARD_1:30; end; assume G.numComponents() = 1; then consider V being object such that A1: G.componentSet() = {V} by CARD_2:42; reconsider V as set by TARSKI:1; now let v be object; assume v in the_Vertices_of G; then reconsider v9=v as Vertex of G; now set V2 = G.reachableFrom(v9); assume A2: not v in V; V2 in G.componentSet() by Def8; then not v in V2 by A1,A2,TARSKI:def 1; hence contradiction by Lm1; end; hence v in V; end; then A3: the_Vertices_of G c= V; V in G.componentSet() by A1,TARSKI:def 1; then V = the_Vertices_of G by A3,XBOOLE_0:def 10; hence thesis by A1,Lm11; end; Lm19: 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() proof let G be connected _Graph, v be Vertex of G; hereby assume v is non cut-vertex; then consider G3 being removeVertex of G,v such that A1: not G.numComponents() in G3.numComponents(); let G2 be removeVertex of G,v; G3.numComponents() c= G.numComponents() by A1,CARD_1:4; hence G2.numComponents() c= G.numComponents() by Lm12,GLIB_000:93; end; assume A2: for G2 being removeVertex of G,v holds G2.numComponents() c= G .numComponents(); now set X = the removeVertex of G,v; assume for G3 being removeVertex of G,v holds G.numComponents() in G3 .numComponents(); then A3: G.numComponents() in X.numComponents(); X.numComponents() c= G.numComponents() by A2; hence contradiction by A3,CARD_1:4; end; hence thesis; end; Lm20: 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 proof let G be connected _Graph, v be Vertex of G, G2 be removeVertex of G,v; assume A1: not v is cut-vertex; G.numComponents() = 1 by Lm18; then G2.numComponents() c= succ 0 by A1,Lm19; then G2.numComponents() c= {} \/ {{}}; then G2.numComponents() = {} \/ {{}} by ZFMISC_1:33 .= succ 0 .= 1; hence thesis by Lm18; end; Lm21: 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 proof let G be non trivial finite connected _Graph; defpred P[Nat] means for G being non trivial finite connected _Graph st G .order() = $1 holds ex v1,v2 being Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex; now let k be Nat; assume A1: for n being Nat st n < k holds P[n]; now let G be non trivial finite connected _Graph such that A2: G.order() = k; A3: G.numComponents() = 1 by Lm18; now per cases; suppose A4: not ex v being Vertex of G st v is cut-vertex; consider v1,v2 being Vertex of G such that A5: v1 <> v2 by GLIB_000:21; take v1,v2; thus v1 <> v2 by A5; thus not v1 is cut-vertex & not v2 is cut-vertex by A4; end; suppose ex cv being Vertex of G st cv is cut-vertex; then consider cv being Vertex of G such that A6: cv is cut-vertex; set G2 = the removeVertex of G,cv; 1 < G2.numComponents() by A3,A6; then 1+1 <= G2.numComponents() by NAT_1:13; then card 2 <= card G2.componentSet(); then Segm card 2 c= Segm card G2.componentSet() by NAT_1:39; then 2 c= card G2.componentSet(); then consider C1,C2 being object such that A7: C1 in G2.componentSet() & C2 in G2.componentSet() and A8: C1 <> C2 by PENCIL_1:2; reconsider C1,C2 as Element of G2.componentSet() by A7; set CC1 = the inducedSubgraph of G2,C1; set CC2 = the inducedSubgraph of G2,C2; A9: the_Vertices_of G2 = (the_Vertices_of G) \ {cv} by GLIB_000:47; G.edgesBetween( (the_Vertices_of G) \ {cv} ) = (the_Edges_of G) \ (G.edgesInOut({cv})) by GLIB_000:35; then G.edgesBetween( (the_Vertices_of G) \ {cv} ) = (the_Edges_of G) \ cv.edgesInOut() by GLIB_000:def 40; then A10: the_Edges_of G2 = (the_Edges_of G) \ cv.edgesInOut() by GLIB_000:47; A11: G2.order() + 1 = k by A2,GLIB_000:48; A12: now let C be Component of G2; now set x = the Vertex of C; assume A13: for a being Vertex of C holds not ex e being set st e Joins cv,a,G; the_Vertices_of C c= the_Vertices_of G2; then reconsider x9=x as Vertex of G2; the_Vertices_of G2 c= the_Vertices_of G; then reconsider x99=x9 as Vertex of G; consider W being Walk of G such that A14: W is_Walk_from cv,x99 by Def1; set P = the Path of W; A15: P is_Walk_from cv,x99 by A14,GLIB_001:160; then A16: P.first() = cv by GLIB_001:def 23; set P2 = P.cut(2*1+1, len P); A17: 1 <= len P by ABIAN:12; A18: P.last() = x by A15,GLIB_001:def 23; then A19: P.(len P)=x by GLIB_001:def 7; not x9 in {cv} by A9,XBOOLE_0:def 5; then A20: x <> cv by TARSKI:def 1; then A21: P is non trivial by A16,A18,GLIB_001:127; then A22: 2*1+1 <= len P by GLIB_001:125; then P2 is_Walk_from P.3, P.(len P) by GLIB_001:37; then A23: P2 is_Walk_from P.3, x by A18,GLIB_001:def 7; A24: P.(2*0+1)=cv by A16,GLIB_001:def 6; now assume cv in P2.vertices(); then consider n being odd Element of NAT such that A25: n <= len P2 and A26: P2.n = cv by GLIB_001:87; A27: 1 <= n by ABIAN:12; then A28: 1+0 < n+2 by XREAL_1:8; A29: n in dom P2 by A25,A27,FINSEQ_3:25; then 3+n-1 in dom P by A22,GLIB_001:47; then A30: 2+n <= len P by FINSEQ_3:25; P.(3+n-1) = cv by A22,A26,A29,GLIB_001:47; hence contradiction by A20,A24,A19,A30,A28,GLIB_001:def 28; end; then reconsider P2 as Walk of G2 by GLIB_001:171; P2 is_Walk_from P.3, x by A23,GLIB_001:19; then P2.reverse() is_Walk_from x,P.3 by GLIB_001:23; then A31: P.3 in G2.reachableFrom(x9) by Def5; len P <> 1 by A21,GLIB_001:125; then 2*0+1 < len P by A17,XXREAL_0:1; then P.(1+1) Joins P.1,P.(1+2),G by GLIB_001:def 3; then A32: P.2 Joins cv, P.3, G by A16,GLIB_001:def 6; the_Vertices_of C = G2.reachableFrom(x9) by Lm16; hence contradiction by A13,A32,A31; end; then consider a being Vertex of C, e being set such that A33: e Joins cv,a,G; A34: e in the_Edges_of G by A33,GLIB_000:def 13; now per cases; suppose C is trivial; then consider v99 being Vertex of C such that A35: the_Vertices_of C = {v99} by GLIB_000:22; the_Vertices_of C c= the_Vertices_of G2; then reconsider v9=v99 as Vertex of G2; reconsider v=v9 as Vertex of G by GLIB_000:42; take v; thus v in the_Vertices_of C; not v9 in {cv} by A9,XBOOLE_0:def 5; then A36: v9 <> cv by TARSKI:def 1; A37: {v9} = G2.reachableFrom(v9) by A35,Lm16; now set G3 = the removeVertex of G,v; A38: now let e, z be set; assume A39: e Joins v,z,G; then A40: e in the_Edges_of G by GLIB_000:def 13; now assume that A41: z <> v and A42: z <> cv; not e in cv.edgesInOut() by A36,A39,A42,GLIB_000:65; then e in the_Edges_of G2 by A10,A40,XBOOLE_0:def 5; then e Joins v,z,G2 by A39,GLIB_000:73; then z in G2.reachableFrom(v9) by Lm1,Lm2; hence contradiction by A37,A41,TARSKI:def 1; end; hence z = v or z = cv; end; now let x,y be Vertex of G3; now per cases; suppose A43: x = y; set W = G3.walkOf(x); take W; thus W is_Walk_from x,y by A43,GLIB_001:13; end; suppose A44: x <> y; reconsider x9=x,y9=y as Vertex of G by GLIB_000:42; consider W being Walk of G such that A45: W is_Walk_from x9,y9 by Def1; set P = the Path of W; A46: P is_Walk_from x9,y9 by A45,GLIB_001:160; A47: the_Vertices_of G3 = (the_Vertices_of G)\{v} by GLIB_000:47; then not x in {v} by XBOOLE_0:def 5; then x <> v by TARSKI:def 1; then A48: v <> P.1 by A46,GLIB_001:17; not y in {v} by A47,XBOOLE_0:def 5; then y <> v by TARSKI:def 1; then A49: v <> P.(len P) by A46,GLIB_001:17; now assume v in P.vertices(); then consider n being odd Element of NAT such that A50: n <= len P and A51: P.n = v by GLIB_001:87; 1 <= n by ABIAN:12; then 1 < n by A48,A51,XXREAL_0:1; then 1+1 <= n by NAT_1:13; then reconsider n2 = n-2*1 as odd Element of NAT by INT_1:5; A52: now A53: n2 < n - 0 by XREAL_1:15; assume P.n2 = v; hence contradiction by A48,A50,A51,A53, GLIB_001:def 28; end; set e1 = P.(n2+1), e2 = P.(n+1); n - 2 < len P - 0 by A50,XREAL_1:15; then e1 Joins P.n2, P.(n2+2), G by GLIB_001:def 3; then A54: P.n2 = cv by A38,A51,A52,GLIB_000:14; A55: n < len P by A49,A50,A51,XXREAL_0:1; then A56: n+2 <= len P by GLIB_001:1; A57: now A58: n+0 < n+2 by XREAL_1:8; assume P.(n+2) = v; hence contradiction by A48,A51,A56,A58, GLIB_001:def 28; end; n2 < n - 0 by XREAL_1:15; then A59: n2+0 < n+2 by XREAL_1:8; e2 Joins v, P.(n+2), G by A51,A55,GLIB_001:def 3; then A60: P.(n+2) = cv by A38,A57; then cv = P.1 by A54,A56,A59,GLIB_001:def 28; then A61: cv = x by A46,GLIB_001:17; cv = P.(len P) by A54,A56,A60,A59,GLIB_001:def 28; hence contradiction by A44,A46,A61,GLIB_001:17; end; then reconsider P as Walk of G3 by GLIB_001:171; take P; thus P is_Walk_from x,y by A46,GLIB_001:19; end; end; hence ex P being Walk of G3 st P is_Walk_from x,y; end; then A62: G3 is connected; assume v is cut-vertex; then 1 < G3.numComponents() by A3; hence contradiction by A62,Lm18; end; hence not v is cut-vertex; end; suppose C is non trivial; then reconsider C9=C as non trivial _Graph; C.order()+0 < G2.order()+1 by GLIB_000:75,XREAL_1:8; then consider v1, v2 being Vertex of C9 such that A63: v1 <> v2 and A64: not v1 is cut-vertex and A65: not v2 is cut-vertex by A1,A11; set C9R1 = the removeVertex of C9,v1; A66: C9R1 is connected by A64,Lm20; set C9R2 = the removeVertex of C9,v2; A67: the_Vertices_of C9R1 = (the_Vertices_of C9) \ {v1} by GLIB_000:47; v2 in the_Vertices_of G2 by GLIB_000:42; then not v2 in {cv} by A9,XBOOLE_0:def 5; then A68: v2 <> cv by TARSKI:def 1; A69: the_Vertices_of C9R2 = (the_Vertices_of C9) \ {v2} by GLIB_000:47; v1 in the_Vertices_of G2 by GLIB_000:42; then not v1 in {cv} by A9,XBOOLE_0:def 5; then A70: v1 <> cv by TARSKI:def 1; A71: C9R2 is connected by A65,Lm20; now per cases; suppose A72: not v1 in cv.allNeighbors(); reconsider v9=v1 as Vertex of G2 by GLIB_000:42; reconsider v =v9 as Vertex of G by GLIB_000:42; take v; thus v in the_Vertices_of C; set G3 = the removeVertex of G,v; A73: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:47; not cv in {v} by A70,TARSKI:def 1; then reconsider cv9 = cv as Vertex of G3 by A73, XBOOLE_0:def 5; A74: v1 <> a by A33,A72,GLIB_000:71; A75: the_Vertices_of C = G2.reachableFrom(v9) by Lm16; now let y be Vertex of G3; now per cases; suppose y = cv; then G3.walkOf(y) is_Walk_from cv9,y by GLIB_001:13; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; suppose A76: y <> cv; now per cases; suppose A77: y in the_Vertices_of C; not a in {v1} by A74,TARSKI:def 1; then A78: a in the_Vertices_of C9R1 by A67,XBOOLE_0:def 5; not y in {v1} by A73,XBOOLE_0:def 5; then y in the_Vertices_of C9R1 by A67,A77, XBOOLE_0:def 5; then consider W being Walk of C9R1 such that A79: W is_Walk_from y,a by A66,A78; A80: W.1 = y & W.(len W) = a by A79,GLIB_001:17; A81: now assume v in W.vertices(); then not v in {v1} by A67,XBOOLE_0:def 5; hence contradiction by TARSKI:def 1; end; not e in v.edgesInOut() by A33,A70,A74, GLIB_000:65; then e in (the_Edges_of G)\v.edgesInOut() by A34, XBOOLE_0:def 5; then e in (the_Edges_of G)\G.edgesInOut({v}) by GLIB_000:def 40; then e in G.edgesBetween((the_Vertices_of G)\{v }) by GLIB_000:35; then e in the_Edges_of G3 by GLIB_000:47; then e Joins cv,a,G3 by A33,GLIB_000:73; then A82: e Joins a,cv,G3 by GLIB_000:14; reconsider W as Walk of C by GLIB_001:167; reconsider W as Walk of G2 by GLIB_001:167; reconsider W as Walk of G by GLIB_001:167; not v in W.vertices() by A81,GLIB_001:98; then reconsider W as Walk of G3 by GLIB_001:171; W is_Walk_from y,a by A80,GLIB_001:17; then W.addEdge(e) is_Walk_from y,cv by A82, GLIB_001:66; then W.addEdge(e).reverse() is_Walk_from cv,y by GLIB_001:23; hence ex W being Walk of G3 st W is_Walk_from cv9 ,y; end; suppose A83: not y in the_Vertices_of C; reconsider y9=y as Vertex of G by GLIB_000:42; consider W being Walk of G such that A84: W is_Walk_from cv,y9 by Def1; set P = the Path of W; A85: P is_Walk_from cv,y9 by A84,GLIB_001:160; then A86: P.(len P) = y9 by GLIB_001:17; A87: P.1 = cv by A85,GLIB_001:17; now assume v in P.vertices(); then consider n being odd Element of NAT such that A88: n <= len P and A89: P.n = v by GLIB_001:87; set P2 = P.cut(n,len P); A90: P2 is_Walk_from v, y9 by A86,A88,A89, GLIB_001:37; 1 <= n by ABIAN:12; then A91: 1 < n by A70,A87,A89,XXREAL_0:1; now assume cv in P2.vertices(); then consider m being odd Element of NAT such that A92: m <= len P2 and A93: P2.m = cv by GLIB_001:87; 1 <= m by ABIAN:12; then A94: m in dom P2 by A92,FINSEQ_3:25; then A95: P.(n+m-1) = cv by A88,A93,GLIB_001:47; 1+1 < n+m by A91,ABIAN:12,XREAL_1:8; then 1+1-1 < n+m-1 by XREAL_1:14; then A96: 2*0+1 < n+m-1; A97: n+m-1 in dom P by A88,A94,GLIB_001:47; then n+m-1 <= len P by FINSEQ_3:25; hence contradiction by A76,A87,A86,A95,A97 ,A96,GLIB_001:def 28; end; then reconsider P2 as Walk of G2 by GLIB_001:171; P2 is_Walk_from v,y9 by A90,GLIB_001:19; hence contradiction by A75,A83,Def5; end; then reconsider P as Walk of G3 by GLIB_001:171; take P; thus P is_Walk_from cv9,y by A85,GLIB_001:19; end; end; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; end; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; then G3 is connected by Lm6; then G3.numComponents() = 1 by Lm18; hence not v is cut-vertex by A3; end; suppose A98: v1 in cv.allNeighbors() & not v2 in cv .allNeighbors(); reconsider v9=v2 as Vertex of G2 by GLIB_000:42; reconsider v =v9 as Vertex of G by GLIB_000:42; take v; thus v in the_Vertices_of C; set G3 = the removeVertex of G,v; A99: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:47; not cv in {v} by A68,TARSKI:def 1; then reconsider cv9 = cv as Vertex of G3 by A99, XBOOLE_0:def 5; A100: v2 <> a by A33,A98,GLIB_000:71; A101: the_Vertices_of C = G2.reachableFrom(v9) by Lm16; now let y be Vertex of G3; now per cases; suppose y = cv; then G3.walkOf(y) is_Walk_from cv9,y by GLIB_001:13; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; suppose A102: y <> cv; now per cases; suppose A103: y in the_Vertices_of C; not a in {v2} by A100,TARSKI:def 1; then A104: a in the_Vertices_of C9R2 by A69,XBOOLE_0:def 5; not y in {v2} by A99,XBOOLE_0:def 5; then y in the_Vertices_of C9R2 by A69,A103, XBOOLE_0:def 5; then consider W being Walk of C9R2 such that A105: W is_Walk_from y,a by A71,A104; A106: W.1 = y & W.(len W) = a by A105,GLIB_001:17; A107: now assume v in W.vertices(); then not v in {v2} by A69,XBOOLE_0:def 5; hence contradiction by TARSKI:def 1; end; not e in v.edgesInOut() by A33,A68,A100, GLIB_000:65; then e in (the_Edges_of G) \ v.edgesInOut() by A34,XBOOLE_0:def 5; then e in (the_Edges_of G)\G.edgesInOut({v}) by GLIB_000:def 40; then e in G.edgesBetween(the_Vertices_of G\{v}) by GLIB_000:35; then e in the_Edges_of G3 by GLIB_000:47; then e Joins cv,a,G3 by A33,GLIB_000:73; then A108: e Joins a,cv,G3 by GLIB_000:14; reconsider W as Walk of C by GLIB_001:167; reconsider W as Walk of G2 by GLIB_001:167; reconsider W as Walk of G by GLIB_001:167; not v in W.vertices() by A107,GLIB_001:98; then reconsider W as Walk of G3 by GLIB_001:171; W is_Walk_from y,a by A106,GLIB_001:17; then W.addEdge(e) is_Walk_from y,cv by A108, GLIB_001:66; then W.addEdge(e).reverse() is_Walk_from cv,y by GLIB_001:23; hence ex W being Walk of G3 st W is_Walk_from cv9 ,y; end; suppose A109: not y in the_Vertices_of C; reconsider y9=y as Vertex of G by GLIB_000:42; consider W being Walk of G such that A110: W is_Walk_from cv,y9 by Def1; set P = the Path of W; A111: P is_Walk_from cv,y9 by A110,GLIB_001:160; then A112: P.(len P) = y9 by GLIB_001:17; A113: P.1 = cv by A111,GLIB_001:17; now assume v in P.vertices(); then consider n being odd Element of NAT such that A114: n <= len P and A115: P.n = v by GLIB_001:87; set P2 = P.cut(n,len P); A116: P2 is_Walk_from v, y9 by A112,A114,A115, GLIB_001:37; 1 <= n by ABIAN:12; then A117: 1 < n by A68,A113,A115,XXREAL_0:1; now assume cv in P2.vertices(); then consider m being odd Element of NAT such that A118: m <= len P2 and A119: P2.m = cv by GLIB_001:87; 1 <= m by ABIAN:12; then A120: m in dom P2 by A118,FINSEQ_3:25; then A121: P.(n+m-1) = cv by A114,A119,GLIB_001:47; 1+1 < n+m by A117,ABIAN:12,XREAL_1:8; then 1+1-1 < n+m-1 by XREAL_1:14; then A122: 2*0+1 < n+m-1; A123: n+m-1 in dom P by A114,A120,GLIB_001:47; then n+m-1 <= len P by FINSEQ_3:25; hence contradiction by A102,A113,A112,A121 ,A123,A122,GLIB_001:def 28; end; then reconsider P2 as Walk of G2 by GLIB_001:171; P2 is_Walk_from v,y9 by A116,GLIB_001:19; hence contradiction by A101,A109,Def5; end; then reconsider P as Walk of G3 by GLIB_001:171; take P; thus P is_Walk_from cv9,y by A111,GLIB_001:19; end; end; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; end; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; then G3 is connected by Lm6; then G3.numComponents() = 1 by Lm18; hence not v is cut-vertex by A3; end; suppose v1 in cv.allNeighbors() & v2 in cv .allNeighbors(); then consider e being object such that A124: e Joins cv,v2,G by GLIB_000:71; reconsider v9=v1 as Vertex of G2 by GLIB_000:42; set a = v2; reconsider v =v9 as Vertex of G by GLIB_000:42; take v; thus v in the_Vertices_of C; set G3 = the removeVertex of G,v; A125: the_Vertices_of G3 = (the_Vertices_of G) \ {v} by GLIB_000:47; not cv in {v} by A70,TARSKI:def 1; then reconsider cv9 = cv as Vertex of G3 by A125, XBOOLE_0:def 5; A126: the_Vertices_of C = G2.reachableFrom(v9) by Lm16; A127: e in the_Edges_of G by A124,GLIB_000:def 13; now let y be Vertex of G3; now per cases; suppose y = cv; then G3.walkOf(y) is_Walk_from cv9,y by GLIB_001:13; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; suppose A128: y <> cv; now per cases; suppose A129: y in the_Vertices_of C; not a in {v1} by A63,TARSKI:def 1; then A130: a in the_Vertices_of C9R1 by A67,XBOOLE_0:def 5; not y in {v1} by A125,XBOOLE_0:def 5; then y in the_Vertices_of C9R1 by A67,A129, XBOOLE_0:def 5; then consider W being Walk of C9R1 such that A131: W is_Walk_from y,a by A66,A130; A132: W.1 = y & W.(len W) = a by A131,GLIB_001:17; A133: now assume v in W.vertices(); then not v in {v1} by A67,XBOOLE_0:def 5; hence contradiction by TARSKI:def 1; end; not e in v.edgesInOut() by A63,A70,A124, GLIB_000:65; then e in (the_Edges_of G)\v.edgesInOut() by A127 ,XBOOLE_0:def 5; then e in (the_Edges_of G)\G.edgesInOut({v}) by GLIB_000:def 40; then e in G.edgesBetween(the_Vertices_of G\{v}) by GLIB_000:35; then e in the_Edges_of G3 by GLIB_000:47; then e Joins cv,a,G3 by A124,GLIB_000:73; then A134: e Joins a,cv,G3 by GLIB_000:14; reconsider W as Walk of C by GLIB_001:167; reconsider W as Walk of G2 by GLIB_001:167; reconsider W as Walk of G by GLIB_001:167; not v in W.vertices() by A133,GLIB_001:98; then reconsider W as Walk of G3 by GLIB_001:171; W is_Walk_from y,a by A132,GLIB_001:17; then W.addEdge(e) is_Walk_from y,cv by A134, GLIB_001:66; then W.addEdge(e).reverse() is_Walk_from cv,y by GLIB_001:23; hence ex W being Walk of G3 st W is_Walk_from cv9 ,y; end; suppose A135: not y in the_Vertices_of C; reconsider y9=y as Vertex of G by GLIB_000:42; consider W being Walk of G such that A136: W is_Walk_from cv,y9 by Def1; set P = the Path of W; A137: P is_Walk_from cv,y9 by A136,GLIB_001:160; then A138: P.(len P) = y9 by GLIB_001:17; A139: P.1 = cv by A137,GLIB_001:17; now assume v in P.vertices(); then consider n being odd Element of NAT such that A140: n <= len P and A141: P.n = v by GLIB_001:87; set P2 = P.cut(n,len P); A142: P2 is_Walk_from v, y9 by A138,A140,A141, GLIB_001:37; 1 <= n by ABIAN:12; then A143: 1 < n by A70,A139,A141,XXREAL_0:1; now assume cv in P2.vertices(); then consider m being odd Element of NAT such that A144: m <= len P2 and A145: P2.m = cv by GLIB_001:87; 1 <= m by ABIAN:12; then A146: m in dom P2 by A144,FINSEQ_3:25; then A147: P.(n+m-1) = cv by A140,A145,GLIB_001:47; 1+1 < n+m by A143,ABIAN:12,XREAL_1:8; then 1+1-1 < n+m-1 by XREAL_1:14; then A148: 2*0+1 < n+m-1; A149: n+m-1 in dom P by A140,A146,GLIB_001:47; then n+m-1 <= len P by FINSEQ_3:25; hence contradiction by A128,A139,A138,A147 ,A149,A148,GLIB_001:def 28; end; then reconsider P2 as Walk of G2 by GLIB_001:171; P2 is_Walk_from v,y9 by A142,GLIB_001:19; hence contradiction by A126,A135,Def5; end; then reconsider P as Walk of G3 by GLIB_001:171; take P; thus P is_Walk_from cv9,y by A137,GLIB_001:19; end; end; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; end; hence ex W being Walk of G3 st W is_Walk_from cv9,y; end; then G3 is connected by Lm6; then G3.numComponents() = 1 by Lm18; hence not v is cut-vertex by A3; end; end; hence ex v being Vertex of G st v in the_Vertices_of C & not v is cut-vertex; end; end; hence ex v being Vertex of G st v in the_Vertices_of C & not v is cut-vertex; end; then consider v1 being Vertex of G such that A150: v1 in the_Vertices_of CC1 and A151: not v1 is cut-vertex; consider v2 being Vertex of G such that A152: v2 in the_Vertices_of CC2 and A153: not v2 is cut-vertex by A12; take v1,v2; now C2 is non empty Subset of the_Vertices_of G2 by Lm13; then A154: the_Vertices_of CC2 = C2 by GLIB_000:def 37; C1 is non empty Subset of the_Vertices_of G2 by Lm13; then A155: the_Vertices_of CC1 = C1 by GLIB_000:def 37; assume v1 = v2; then CC1 == CC2 by A150,A152,Lm17; hence contradiction by A8,A155,A154,GLIB_000:def 34; end; hence v1 <> v2; thus not v1 is cut-vertex & not v2 is cut-vertex by A151,A153; end; end; hence ex v1,v2 being Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex; end; hence P[k]; end; then A156: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]; A157: for k being Nat holds P[k] from NAT_1:sch 4(A156); G.order() = G.order(); hence thesis by A157; end; registration let G be non trivial finite connected _Graph; cluster non cut-vertex for Vertex of G; existence proof ex v1,v2 being Vertex of G st v1 <> v2 &( not v1 is cut-vertex)& not v2 is cut-vertex by Lm21; hence thesis; end; end; Lm22: 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 proof let G be acyclic _Graph, W be Path of G, e be set; assume that A1: not e in W.edges() and A2: e in W.last().edgesInOut(); set v = W.last().adj(e), W2 = W.addEdge(e); A3: e Joins W.last(), W.last().adj(e), G by A2,GLIB_000:67; then A4: len W2 = len W + 2 by GLIB_001:64; A5: W2 is Trail-like by A1,A2,GLIB_001:142; now per cases; suppose A6: W is trivial; then for n being odd Element of NAT st 1 < n & n <= len W holds W.n <> v by GLIB_001:126; hence thesis by A1,A3,A6,GLIB_001:150; end; suppose A7: W is non trivial; A8: now let n be odd Element of NAT; assume that A9: 1 < n and A10: n <= len W; now set W3 = W2.cut(n,len W2); assume A11: W.n = v; A12: n <= len W2 by A4,A10,NAT_1:12; then A13: W3.first()=W2.n by GLIB_001:37; now assume W3 is trivial; then len W3 = 1 by GLIB_001:126; then 1 + n = len W2 + 1 by A12,GLIB_001:36; then 2 + len W - len W <= len W - len W by A4,A10,XREAL_1:13; then 2 <= 0; hence contradiction; end; then consider W4 being Path of W3 such that A14: W4 is non trivial by A5,GLIB_001:166; W3.last()=W2.(len W2) by A12,GLIB_001:37; then A15: W3.last() = W2.last() by GLIB_001:def 7 .= v by A3,GLIB_001:63; n in dom W by A9,A10,FINSEQ_3:25; then W3.first() = v by A3,A11,A13,GLIB_001:65; then W4 is_Walk_from v,v by A15,GLIB_001:def 32; then W4 is closed by GLIB_001:119; then W4 is Cycle-like by A14,GLIB_001:def 31; hence contradiction by Def2; end; hence W.n <> v; end; W is not closed by A7,GLIB_001:def 31,Def2; hence thesis by A1,A3,A8,GLIB_001:150; end; end; hence thesis; end; Lm23: 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) proof let G be non trivial finite acyclic _Graph such that A1: the_Edges_of G <> {}; defpred P[Nat] means ex W being Path of G st len W = $1; set e = the Element of the_Edges_of G; A2: now let k be Nat; assume P[k]; then consider P being Path of G such that A3: len P = k; 2*len P.vertexSeq() <= 2*(G.order()+1) by GLIB_001:154,XREAL_1:64; then k + 1 <= 2*(G.order() + 1) by A3,GLIB_001:def 14; then k+1-1 <= 2*(G.order() + 1) - 0 by XREAL_1:13; hence k <= 2*(G.order()+1); end; set src = (the_Source_of G).e, tar = (the_Target_of G).e; e Joins src,tar,G by A1,GLIB_000:def 13; then A4: len G.walkOf(src,e,tar) = 3 by GLIB_001:14; then A5: ex k being Nat st P[k]; consider k being Nat such that A6: P[k] & for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A2,A5 ); consider W being Path of G such that A7: len W = k and A8: for n being Nat st P[n] holds n <= k by A6; A9: len W.reverse() = k by A7,GLIB_001:21; A10: 3 <= len W by A4,A7,A8; then A11: W is non trivial by GLIB_001:125; A12: now assume W.first() = W.last(); then W is closed by GLIB_001:def 24; then W is Cycle-like by A11,GLIB_001:def 31; hence contradiction by Def2; end; then A13: W is open by GLIB_001:def 24; A14: now let W be Path of G; assume that A15: len W = k and A16: W is open; 2+1 <= len W by A4,A8,A15; then 2 < len W by NAT_1:13; then reconsider lenW2 = len W - 2*1 as odd Element of NAT by INT_1:5; A17: lenW2 + 2 = len W; A18: W is non trivial by A7,A10,A15,GLIB_001:125; now W.last() in W.vertices() by GLIB_001:88; then not W.last() is isolated by A18,GLIB_001:135; then W.last().degree() <> 0 by GLIB_000:def 50; then card W.last().edgesInOut() <> 0 by GLIB_000:19; then 0 < card W.last().edgesInOut() by NAT_1:3; then A19: 0+1 <= card W.last().edgesInOut() by NAT_1:13; assume not W.last() is endvertex; then W.last().degree() <> 1 by GLIB_000:def 52; then card W.last().edgesInOut() <> 1 by GLIB_000:19; then 1 < card W.last().edgesInOut() by A19,XXREAL_0:1; then consider e1,e2 being set such that A20: e1 in W.last().edgesInOut() and A21: e2 in W.last().edgesInOut() & e1 <> e2 by NAT_1:59; now per cases; suppose A22: e1 = W.(lenW2+1); take e2; thus e2 in W.last().edgesInOut() & e2 <> W.(lenW2+1) by A21,A22; end; suppose A23: e1 <> W.(lenW2+1); take e1; thus e1 in W.last().edgesInOut() & e1 <> W.(lenW2+1) by A20,A23; end; end; then consider e being set such that A24: e in W.last().edgesInOut() and A25: e <> W.(lenW2+1); consider v being Vertex of G such that A26: e Joins W.last(),v,G by A24,GLIB_000:64; now per cases; suppose v in W.vertices(); then consider n being odd Element of NAT such that A27: n <= len W and A28: W.n = v by GLIB_001:87; set m = W.rfind(n); set W2 = W.cut(m,len W); A29: m <= len W by A27,GLIB_001:def 22; then W2.last() = W.(len W) by GLIB_001:37; then A30: e Joins W2.last(),v,G by A26,GLIB_001:def 7; W.m = v by A27,A28,GLIB_001:def 22; then A31: W2.first() = v by A29,GLIB_001:37; A32: e in W2.last().edgesInOut() by A30,GLIB_000:62; now per cases; suppose A33: not e in W2.edges(); A34: W2.addEdge(e) is non trivial by A30,GLIB_001:132; W2.addEdge(e).first() = v & W2.addEdge(e).last() = v by A31,A30, GLIB_001:63; then A35: W2.addEdge(e) is closed by GLIB_001:def 24; W2.addEdge(e) is Path-like by A32,A33,Lm22; then W2.addEdge(e) is Cycle-like by A35,A34,GLIB_001:def 31; hence contradiction by Def2; end; suppose A36: e in W2.edges(); W2.edges() c= W.edges() by GLIB_001:106; then consider a being even Element of NAT such that A37: 1 <= a and A38: a <= len W and A39: W.a = e by A36,GLIB_001:99; reconsider a1 = a - 1 as odd Element of NAT by A37,INT_1:5; A40: a1 < len W-0 by A38,XREAL_1:15; a < lenW2 + 2 by A38,XXREAL_0:1; then a+1 <= lenW2+1+1 by NAT_1:13; then a <= lenW2+1 by XREAL_1:6; then A41: a < lenW2+1 by A25,A39,XXREAL_0:1; a1+1 = a; then A42: e Joins W.a1, W.(a1+2), G by A39,A40,GLIB_001:def 3; now per cases by A26,A42,GLIB_000:15; suppose W.last() = W.a1 & v = W.(a1+2); then W.(len W) = W.a1 by GLIB_001:def 7; hence contradiction by A16,A40,GLIB_001:147; end; suppose A43: W.last() = W.(a1+2) & v = W.a1; a1 < lenW2+1-1 by A41,XREAL_1:14; then A44: a1+2 < len W by A17,XREAL_1:8; W.(len W) = W.(a1+2) by A43,GLIB_001:def 7; hence contradiction by A16,A44,GLIB_001:147; end; end; hence contradiction; end; end; hence contradiction; end; suppose A45: not v in W.vertices(); A46: len W.addEdge(e) = k + 2 by A15,A26,GLIB_001:64; W.addEdge(e) is Path-like by A16,A26,A45,GLIB_001:151; then k+2 <= k+0 by A8,A46; hence contradiction by XREAL_1:6; end; end; hence contradiction; end; hence W.last() is endvertex; end; W is_Walk_from W.first(),W.last() by GLIB_001:def 23; then A47: W.last() in G.reachableFrom(W.first()) by Def5; W.reverse() is open by A13,GLIB_001:120; then W.reverse().last() is endvertex by A14,A9; then A48: W.first() is endvertex by GLIB_001:22; W.last() is endvertex by A7,A13,A14; hence thesis by A12,A48,A47; end; Lm24: 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 proof let G be non trivial finite Tree-like _Graph; consider v1, v2 being Vertex of G such that A1: v1 <> v2 by GLIB_000:21; consider W being Walk of G such that A2: W is_Walk_from v1,v2 by Def1; A3: now assume len W = 1; then A4: W.last() = W.1 by GLIB_001:def 7 .= W.first() by GLIB_001:def 6; W.first() = v1 by A2,GLIB_001:def 23; hence contradiction by A1,A2,A4,GLIB_001:def 23; end; 1 <= len W by ABIAN:12; then 1 < len W by A3,XXREAL_0:1; then 1+1 <= len W by NAT_1:13; then 1+1 in dom W by FINSEQ_3:25; then W.(2*1) in the_Edges_of G by GLIB_001:8; then ex v1,v2 being Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G.reachableFrom(v1) by Lm23; hence thesis; end; registration let G be non trivial finite Tree-like _Graph; cluster endvertex for Vertex of G; existence proof consider v1,v2 being Vertex of G such that v1 <> v2 and A1: v1 is endvertex and v2 is endvertex by Lm24; take v1; thus thesis by A1; end; 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; coherence by Lm5; end; definition let GF be Graph-yielding Function; attr GF is connected means 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 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 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 :Def12b: for x being Element of dom GF holds GF.x is connected; compatibility proof hereby assume A1: GF is connected; let x be Element of dom GF; consider G being _Graph such that A2: GF.x = G & G is connected by A1; thus GF.x is connected by A2; end; assume A3: for x being Element of dom GF holds GF.x is connected; let x be object; assume x in dom GF; then reconsider y = x as Element of dom GF; take GF.y; thus thesis by A3; end; redefine attr GF is acyclic means :Def13b: for x being Element of dom GF holds GF.x is acyclic; compatibility proof hereby assume A1: GF is acyclic; let x be Element of dom GF; consider G being _Graph such that A2: GF.x = G & G is acyclic by A1; thus GF.x is acyclic by A2; end; assume A3: for x being Element of dom GF holds GF.x is acyclic; let x be object; assume x in dom GF; then reconsider y = x as Element of dom GF; take GF.y; thus thesis by A3; end; redefine attr GF is Tree-like means for x being Element of dom GF holds GF.x is Tree-like; compatibility proof hereby assume A1: GF is Tree-like; let x be Element of dom GF; consider G being _Graph such that A2: GF.x = G & G is Tree-like by A1; thus GF.x is Tree-like by A2; end; assume A3: for x being Element of dom GF holds GF.x is Tree-like; let x be object; assume x in dom GF; then reconsider y = x as Element of dom GF; take GF.y; thus thesis by A3; end; end; LmNat: :: copied from GLIB_000 for F being ManySortedSet of NAT, n being object holds n is Nat iff n in dom F proof let F be ManySortedSet of NAT, n being object; hereby assume n is Nat; then n in NAT by ORDINAL1:def 12; hence n in dom F by PARTFUN1:def 2; end; assume n in dom F; then n in NAT by PARTFUN1:def 2; hence n is Nat; end; definition let GSq be GraphSeq; redefine attr GSq is connected means :Def12: for n being Nat holds GSq.n is connected; compatibility proof hereby assume A1: GSq is connected; let x be Nat; x in dom GSq by LmNat; then x is Element of dom GSq; hence GSq.x is connected by A1; end; assume A2: for x being Nat holds GSq.x is connected; let x be Element of dom GSq; x is Nat by LmNat; hence thesis by A2; end; redefine attr GSq is acyclic means :Def13: for n being Nat holds GSq.n is acyclic; compatibility proof hereby assume A1: GSq is acyclic; let x be Nat; x in dom GSq by LmNat; then x is Element of dom GSq; hence GSq.x is acyclic by A1; end; assume A2: for x being Nat holds GSq.x is acyclic; let x be Element of dom GSq; x is Nat by LmNat; hence thesis by A2; end; redefine attr GSq is Tree-like means for n being Nat holds GSq.n is Tree-like; compatibility proof hereby assume A1: GSq is Tree-like; let x be Nat; x in dom GSq by LmNat; then x is Element of dom GSq; hence GSq.x is Tree-like by A1; end; assume A2: for x being Nat holds GSq.x is Tree-like; let x be Element of dom GSq; x is Nat by LmNat; hence thesis by A2; end; end; registration cluster connected acyclic Tree-like non empty for Graph-yielding Function; existence proof reconsider GSq = NAT --> the Tree-like _Graph as GraphSeq; take GSq; thus thesis; end; end; registration cluster trivial -> connected for Graph-yielding Function; coherence proof let GF be Graph-yielding Function; assume A1: GF is trivial; let x be object; assume x in dom GF; then consider G being _Graph such that A2: GF.x = G & G is trivial by A1, GLIB_000:def 60; take G; thus thesis by A2; end; cluster trivial loopless -> Tree-like for Graph-yielding Function; coherence proof let GF be Graph-yielding Function; assume A1: GF is trivial loopless; let x be object; assume A2: x in dom GF; then consider G being _Graph such that A3: GF.x = G & G is trivial by A1, GLIB_000:def 60; consider G0 being _Graph such that A4: GF.x = G0 & G0 is loopless by A1, A2, GLIB_000:def 59; take G; thus thesis by A3, A4; end; cluster acyclic -> simple for Graph-yielding Function; coherence proof let GF be Graph-yielding Function; assume A1: GF is acyclic; now let x be object; assume x in dom GF; then consider G being _Graph such that A2: GF.x = G & G is acyclic by A1; take G; thus GF.x = G & G is simple by A2; end; hence thesis by GLIB_000:def 64; end; cluster Tree-like -> acyclic connected for Graph-yielding Function; coherence proof let GF be Graph-yielding Function; assume A1: GF is Tree-like; for x being object st x in dom GF ex G being _Graph st GF.x = G & G is acyclic proof let x be object; assume x in dom GF; then consider G being _Graph such that A2: GF.x = G & G is Tree-like by A1; take G; thus thesis by A2; end; hence GF is acyclic; for x being object st x in dom GF ex G being _Graph st GF.x = G & G is connected proof let x be object; assume x in dom GF; then consider G being _Graph such that A2: GF.x = G & G is Tree-like by A1; take G; thus thesis by A2; end; hence thesis; end; cluster acyclic connected -> Tree-like for Graph-yielding Function; coherence proof let GF be Graph-yielding Function; assume A1: GF is acyclic connected; let x be object; assume A2: x in dom GF; then consider G being _Graph such that A3: GF.x = G & G is acyclic by A1; consider G0 being _Graph such that A4: GF.x = G0 & G0 is connected by A1, A2; take G; thus thesis by A3, A4; end; end; registration cluster halting finite Tree-like for GraphSeq; existence proof set G = the finite Tree-like _Graph; set F = NAT --> G; A1: dom F = NAT; reconsider F as ManySortedSet of NAT; reconsider F as GraphSeq; A2: F.(1+1) = G; take F; F.1 = G; hence F is halting by A2,GLIB_000:def 55; now let x be Nat; x in NAT by ORDINAL1:def 12; then F.x in rng F by A1,FUNCT_1:3; then F.x in {G} by FUNCOP_1:8; hence F.x is finite & F.x is Tree-like by TARSKI:def 1; end; hence thesis by GLIB_000:def 74; end; end; registration let GF be connected non empty Graph-yielding Function; let x be Element of dom GF; cluster GF.x -> connected for _Graph; coherence by Def12b; end; registration let GF be acyclic non empty Graph-yielding Function; let x be Element of dom GF; cluster GF.x -> acyclic for _Graph; coherence by Def13b; 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; coherence; end; registration let GSq be connected GraphSeq, n be Nat; cluster GSq.n -> connected for _Graph; coherence by Def12; end; registration let GSq be acyclic GraphSeq, n be Nat; cluster GSq.n -> acyclic for _Graph; coherence by Def13; end; registration let GSq be Tree-like GraphSeq, n be Nat; cluster GSq.n -> Tree-likefor _Graph; coherence; 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 Th1: for G being non trivial connected _Graph, v being Vertex of G holds not v is isolated proof let G be non trivial connected _Graph, v be Vertex of G; consider v1,v2 being Vertex of G such that A1: v1 <> v2 by GLIB_000:21; now per cases; suppose v1 = v; hence ex u being Vertex of G st u <> v by A1; end; suppose v1 <> v; hence ex u being Vertex of G st u <> v; end; end; then consider u being Vertex of G such that A2: u <> v; consider W being Walk of G such that A3: W is_Walk_from u,v by Def1; A4: W.first() = u by A3,GLIB_001:def 23; A5: W.last() = v by A3,GLIB_001:def 23; then v in W.vertices() by GLIB_001:88; hence thesis by A2,A4,A5,GLIB_001:127,135; end; theorem Th2: 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 proof let G1 be non trivial _Graph, v be Vertex of G1, G2 be removeVertex of G1,v; assume that A1: G2 is connected and A2: ex e being set st e in v.edgesInOut() & not e Joins v,v,G1; A3: now let x be Vertex of G1; assume x <> v; then not x in {v} by TARSKI:def 1; then x in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5; hence x in (the_Vertices_of G2) by GLIB_000:47; end; consider e being set such that A4: e in v.edgesInOut() and A5: not e Joins v,v,G1 by A2; set v3 = v.adj(e); v <> v3 by A4,A5,GLIB_000:67; then reconsider v39=v3 as Vertex of G2 by A3; A6: e Joins v,v3,G1 by A4,GLIB_000:67; then A7: e Joins v3,v,G1 by GLIB_000:14; now let v1, v2 be Vertex of G1; now per cases; suppose v1 <> v; then reconsider v19=v1 as Vertex of G2 by A3; now per cases; suppose v2 <> v; then reconsider v29=v2 as Vertex of G2 by A3; consider W9 being Walk of G2 such that A8: W9 is_Walk_from v19,v29 by A1; reconsider W=W9 as Walk of G1 by GLIB_001:167; W is_Walk_from v1,v2 by A8,GLIB_001:19; hence ex W being Walk of G1 st W is_Walk_from v1,v2; end; suppose A9: v2 = v; consider W9 being Walk of G2 such that A10: W9 is_Walk_from v19,v39 by A1; reconsider W=W9 as Walk of G1 by GLIB_001:167; W is_Walk_from v1,v3 by A10,GLIB_001:19; then W.first() = v1 & W.last() = v3 by GLIB_001:def 23; then W.addEdge(e) is_Walk_from v1, v2 by A7,A9,GLIB_001:63; hence ex W being Walk of G1 st W is_Walk_from v1,v2; end; end; hence ex W being Walk of G1 st W is_Walk_from v1,v2; end; suppose A11: v1 = v; now per cases; suppose v2 <> v; then reconsider v29=v2 as Vertex of G2 by A3; set W1 = G1.walkOf(v1,e,v3); consider W29 being Walk of G2 such that A12: W29 is_Walk_from v39,v29 by A1; reconsider W2=W29 as Walk of G1 by GLIB_001:167; A13: W2 is_Walk_from v3, v2 by A12,GLIB_001:19; take W = W1.append(W2); W1 is_Walk_from v1, v3 by A6,A11,GLIB_001:15; hence W is_Walk_from v1,v2 by A13,GLIB_001:31; end; suppose A14: v2 = v; take W = G1.walkOf(v); thus W is_Walk_from v1,v2 by A11,A14,GLIB_001:13; end; end; hence ex W being Walk of G1 st W is_Walk_from v1,v2; end; end; hence ex W being Walk of G1 st W is_Walk_from v1,v2; end; hence thesis; end; theorem 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 by Lm5; theorem Th4: 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 proof let G1 be connected _Graph, W be Walk of G1, e be set, G2 be removeEdge of G1,e; assume that A1: W is Cycle-like and A2: e in W.edges(); reconsider v1 = (the_Source_of G1).e, v2 = (the_Target_of G1).e as Vertex of G1 by A2,FUNCT_2:5; e Joins v1,v2,G1 by A2,GLIB_000:def 13; then consider X being Walk of G1 such that A3: X is_Walk_from v1,v2 and A4: not e in X.edges() by A1,A2,GLIB_001:157; reconsider X2 = X as Walk of G2 by A4,GLIB_001:172; A5: X2 is_Walk_from v1,v2 by A3,GLIB_001:19; then A6: X2.reverse() is_Walk_from v2,v1 by GLIB_001:23; now let u,v be Vertex of G2; the_Vertices_of G2 c= the_Vertices_of G1; then reconsider u9=u,v9=v as Vertex of G1; consider C being Walk of G1 such that A7: C is_Walk_from u9,v9 by Def1; set P = the Path of C; A8: P is_Walk_from u9,v9 by A7,GLIB_001:160; then A9: P.(len P) = v by GLIB_001:17; A10: P.1 = u by A8,GLIB_001:17; now per cases; suppose e in P.edges(); then consider a,b being Vertex of G1, m being odd Element of NAT such that A11: m+2 <= len P and A12: a = P.m and A13: e = P.(m+1) and A14: b = P.(m+2) and A15: e Joins a,b,G1 by GLIB_001:103; set P1 = P.cut(1,m), P2 = P.cut(m+2, len P); A16: m+2-2 < len P - 0 by A11,XREAL_1:15; then A17: m+1 <= len P by NAT_1:13; now assume e in P1.edges(); then consider x being even Element of NAT such that A18: 1 <= x and A19: x <= len P1 and A20: P1.x = e by GLIB_001:99; x <= m by A16,A19,GLIB_001:45; then A21: x < m+1 by NAT_1:13; x in dom P1 by A18,A19,FINSEQ_3:25; then P.x = e by A16,A20,GLIB_001:46; hence contradiction by A13,A17,A18,A21,GLIB_001:138; end; then reconsider P19=P1 as Walk of G2 by GLIB_001:172; now assume e in P2.edges(); then consider x being even Element of NAT such that A22: 1 <= x and A23: x <= len P2 and A24: P2.x = e by GLIB_001:99; reconsider x1 = x-1 as odd Element of NAT by A22,INT_1:5; A25: x1 < len P2 - 0 by A23,XREAL_1:15; then m+2+x1 in dom P by A11,GLIB_001:36; then A26: m+2+x1 <= len P by FINSEQ_3:25; x1+1 = x; then A27: e = P.(m+2+x1) by A11,A24,A25,GLIB_001:36; m+1 < m+1+1 by NAT_1:13; then A28: m+1+0 < m+2+x1 by NAT_1:2,XREAL_1:8; 1 <= m+1 by NAT_1:12; hence contradiction by A13,A27,A26,A28,GLIB_001:138; end; then reconsider P29=P2 as Walk of G2 by GLIB_001:172; reconsider a,b as Vertex of G2 by GLIB_000:51; 1 <= m by ABIAN:12; then P1 is_Walk_from u,a by A10,A12,A16,GLIB_001:37,JORDAN12:2; then A29: P19 is_Walk_from u,a by GLIB_001:19; P2 is_Walk_from b,v by A9,A11,A14,GLIB_001:37; then A30: P29 is_Walk_from b,v by GLIB_001:19; now per cases by A15,GLIB_000:def 13; suppose a = v1 & b = v2; then P19.append(X2) is_Walk_from u,b by A5,A29,GLIB_001:31; then P19.append(X2).append(P29) is_Walk_from u,v by A30,GLIB_001:31 ; hence ex W being Walk of G2 st W is_Walk_from u,v; end; suppose b = v1 & a = v2; then P19.append(X2.reverse()) is_Walk_from u,b by A6,A29, GLIB_001:31; then P19.append(X2.reverse()).append(P29) is_Walk_from u,v by A30, GLIB_001:31; hence ex W being Walk of G2 st W is_Walk_from u,v; end; end; hence ex W being Walk of G2 st W is_Walk_from u,v; end; suppose not e in P.edges(); then reconsider P as Walk of G2 by GLIB_001:172; take P; thus P is_Walk_from u,v by A8,GLIB_001:19; end; end; hence ex W being Walk of G2 st W is_Walk_from u,v; end; hence thesis; end; theorem (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 by Lm6; theorem for G being trivial _Graph holds G is connected; theorem Th7: G1 == G2 & G1 is connected implies G2 is connected proof assume that A1: G1 == G2 and A2: G1 is connected; now let u,v be Vertex of G2; reconsider u9=u,v9=v as Vertex of G1 by A1,GLIB_000:def 34; consider W9 being Walk of G1 such that A3: W9 is_Walk_from u9,v9 by A2; reconsider W = W9 as Walk of G2 by A1,GLIB_001:179; take W; thus W is_Walk_from u,v by A3,GLIB_001:19; end; hence thesis; end; theorem v in G.reachableFrom(v) by Lm1; theorem for e,x,y being object holds x in G.reachableFrom(v1) & e Joins x,y,G implies y in G.reachableFrom( v1) by Lm2; theorem G.edgesBetween(G.reachableFrom(v)) = G.edgesInOut(G.reachableFrom(v)) proof set R = G.reachableFrom(v); now let x be object; set Sx = (the_Source_of G).x, Tx = (the_Target_of G).x; assume A1: x in G.edgesInOut(R); then reconsider Sx, Tx as Vertex of G by FUNCT_2:5; now per cases by A1,GLIB_000:28; suppose A2: Sx in R; then consider W being Walk of G such that A3: W is_Walk_from v,Sx by Def5; now W.last() = Sx by A3,GLIB_001:def 23; then A4: x Joins W.last(), Tx,G by A1,GLIB_000:def 13; assume A5: not Tx in R; W.first() = v by A3,GLIB_001:def 23; then W.addEdge(x) is_Walk_from v, Tx by A4,GLIB_001:63; hence contradiction by A5,Def5; end; then A6: x in G.edgesInto(R) by A1,GLIB_000:def 26; x in G.edgesOutOf(R) by A1,A2,GLIB_000:def 27; then x in G.edgesInto(R) /\ G.edgesOutOf(R) by A6,XBOOLE_0:def 4; hence x in G.edgesBetween(R) by GLIB_000:def 29; end; suppose A7: Tx in R; then consider W being Walk of G such that A8: W is_Walk_from v,Tx by Def5; now W.last() = Tx by A8,GLIB_001:def 23; then A9: x Joins W.last(), Sx,G by A1,GLIB_000:def 13; assume A10: not Sx in R; W.first() = v by A8,GLIB_001:def 23; then W.addEdge(x) is_Walk_from v, Sx by A9,GLIB_001:63; hence contradiction by A10,Def5; end; then A11: x in G.edgesOutOf(R) by A1,GLIB_000:def 27; x in G.edgesInto(R) by A1,A7,GLIB_000:def 26; then x in G.edgesInto(R) /\ G.edgesOutOf(R) by A11,XBOOLE_0:def 4; hence x in G.edgesBetween(R) by GLIB_000:def 29; end; end; hence x in G.edgesBetween(R); end; then G.edgesBetween(R) c= G.edgesInOut(R) & G.edgesInOut(R) c= G .edgesBetween(R) by GLIB_000:33; hence thesis by XBOOLE_0:def 10; end; theorem v1 in G.reachableFrom(v2) implies G.reachableFrom(v1) = G .reachableFrom(v2) by Lm3; theorem v in W.vertices() implies W.vertices() c= G.reachableFrom(v) by Lm4; theorem 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) proof let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2; assume A1: v1 = v2; let v be object; assume v in G2.reachableFrom(v2); then consider W being Walk of G2 such that A2: W is_Walk_from v2,v by Def5; reconsider W2=W as Walk of G1 by GLIB_001:167; W2 is_Walk_from v1,v by A1,A2,GLIB_001:19; hence thesis by Def5; end; theorem (ex v being Vertex of G st G.reachableFrom(v) = the_Vertices_of G) implies G is connected by Lm7; theorem G is connected implies for v being Vertex of G holds G.reachableFrom(v ) = the_Vertices_of G by Lm8; theorem for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Lm9; theorem v in G.reachableDFrom(v) proof G.walkOf(v) is_Walk_from v,v by GLIB_001:13; hence thesis by Def6; end; theorem x in G.reachableDFrom(v1) & e DJoins x,y,G implies y in G .reachableDFrom(v1) proof set RFV = G.reachableDFrom(v1); assume that A1: x in RFV and A2: e DJoins x,y,G; consider W being directed Walk of G such that A3: W is_Walk_from v1,x by A1,Def6; W.addEdge(e) is directed & W.addEdge(e) is_Walk_from v1,y by A2,A3, GLIB_001:123; hence thesis by Def6; end; theorem G.reachableDFrom(v) c= G.reachableFrom(v) proof set RFD = G.reachableDFrom(v); let x be object; assume A1: x in RFD; then reconsider x9=x as Vertex of G; ex W being directed Walk of G st W is_Walk_from v,x9 by A1,Def6; hence thesis by Def5; end; theorem 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) proof let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of G2; assume A1: v1 = v2; let v be object; assume v in G2.reachableDFrom(v2); then consider W being DWalk of G2 such that A2: W is_Walk_from v2,v by Def6; reconsider W as DWalk of G1 by GLIB_001:175; W is_Walk_from v1,v by A1,A2,GLIB_001:19; hence v in G1.reachableDFrom(v1) by Def6; end; theorem for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds G1.reachableDFrom(v1) = G2.reachableDFrom(v2) proof let v1 be Vertex of G1, v2 be Vertex of G2; assume that A1: G1 == G2 and A2: v1 = v2; now let x be object; hereby assume x in G1.reachableDFrom(v1); then consider W being DWalk of G1 such that A3: W is_Walk_from v2,x by A2,Def6; reconsider W2 = W as DWalk of G2 by A1,GLIB_001:179,181; W2 is_Walk_from v2,x by A3,GLIB_001:19; hence x in G2.reachableDFrom(v2) by Def6; end; assume x in G2.reachableDFrom(v2); then consider W being DWalk of G2 such that A4: W is_Walk_from v1,x by A2,Def6; reconsider W2 = W as DWalk of G1 by A1,GLIB_001:179,181; W2 is_Walk_from v1,x by A4,GLIB_001:19; hence x in G1.reachableDFrom(v1) by Def6; end; hence thesis by TARSKI:2; end; theorem for G1 being _Graph, G2 being connected Subgraph of G1 holds G2 is spanning implies G1 is connected by Lm10; theorem union G.componentSet() = the_Vertices_of G proof now let x be object; thus x in union G.componentSet() implies x in the_Vertices_of G; assume x in the_Vertices_of G; then reconsider x9=x as Vertex of G; set Y = G.reachableFrom(x9); x in Y & Y in G.componentSet() by Def8,Lm1; hence x in union G.componentSet() by TARSKI:def 4; end; hence thesis by TARSKI:2; end; theorem G is connected iff G.componentSet() = {the_Vertices_of G} by Lm11; theorem G1 == G2 implies G1.componentSet() = G2.componentSet() by Lm12; theorem x in G.componentSet() implies x is non empty Subset of the_Vertices_of G by Lm13; theorem G is connected iff G.numComponents() = 1 by Lm18; theorem G1 == G2 implies G1.numComponents() = G2.numComponents() by Lm12; theorem G is Component of G iff G is connected proof thus G is Component of G implies G is connected; A1: G is Subgraph of G by GLIB_000:40; A2: now given G2 being connected Subgraph of G such that A3: G c< G2; now per cases by A1,A3,GLIB_000:98; suppose the_Vertices_of G c< the_Vertices_of G2; hence contradiction by XBOOLE_0:def 8; end; suppose the_Edges_of G c< the_Edges_of G2; hence contradiction by XBOOLE_0:def 8; end; end; hence contradiction; end; assume G is connected; hence thesis by A2,Def7,GLIB_000:40; end; theorem for C being Component of G holds the_Edges_of C = G.edgesBetween( the_Vertices_of C) by Lm14; theorem for C1,C2 being Component of G holds the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 by Lm15; theorem 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) by Lm16; theorem 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 by Lm17; theorem 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() by Lm19; theorem 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 by Lm20; theorem 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 by Lm21; theorem Th37: v is cut-vertex implies G is non trivial proof assume A1: v is cut-vertex; now assume G is trivial; then reconsider G9=G as trivial _Graph; set G2 = the removeVertex of G9,v; G9.numComponents() = 1 & G2.numComponents() = 1 by Lm18; then 1 in 1 by A1; hence contradiction; end; hence thesis; end; theorem 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 proof let v1 be Vertex of G1, v2 be Vertex of G2; assume that A1: G1 == G2 and A2: v1 = v2 and A3: v1 is cut-vertex; A4: G1 is non trivial by A3,Th37; then A5: G2 is non trivial by A1,GLIB_000:89; let G2A be removeVertex of G2,v2; set G1A = the removeVertex of G1,v1; G1.numComponents() = G2.numComponents() by A1,Lm12; then A6: G2.numComponents() in G1A.numComponents() by A3; the_Vertices_of G1A = the_Vertices_of G1 \ {v2} by A2,A4,GLIB_000:47 .= the_Vertices_of G2 \ {v2} by A1,GLIB_000:def 34; then A7: the_Vertices_of G2A = the_Vertices_of G1A by A5,GLIB_000:47; G2 is Subgraph of G1 by A1,GLIB_000:87; then A8: G2A is Subgraph of G1 by GLIB_000:43; the_Edges_of G1A = G1.edgesBetween(the_Vertices_of G1 \ {v1}) by A4, GLIB_000:47 .= G1.edgesBetween(the_Vertices_of G2 \ {v2}) by A1,A2,GLIB_000:def 34 .= G2.edgesBetween(the_Vertices_of G2 \ {v2}) by A1,GLIB_000:90; then the_Edges_of G2A = the_Edges_of G1A by A5,GLIB_000:47; hence thesis by A6,A7,A8,Lm12,GLIB_000:86; end; theorem Th39: for G being finite connected _Graph holds G.order() <= G.size() + 1 proof let G be finite connected _Graph; defpred P[finite _Graph] means $1 is connected implies $1.order() <= $1 .size() + 1; A1: now let k be non zero Nat; assume A2: for Gk being finite _Graph st Gk.order() = k holds P[Gk]; let Gk1 be finite _Graph; assume A3: Gk1.order() = k+1; now A4: now assume Gk1.order() = 1; then k+1 = 0+1 by A3; hence contradiction; end; assume Gk1 is connected; then reconsider Gk19 = Gk1 as non trivial finite connected _Graph by A4, GLIB_000:26; consider v1,v2 being Vertex of Gk19 such that v1 <> v2 and A5: not v1 is cut-vertex and not v2 is cut-vertex by Lm21; set Gkb = the removeVertex of Gk19, v1; A6: Gkb.order() + 1 = k + 1 & Gkb.size()+card v1.edgesInOut()=Gk1 .size() by A3,GLIB_000:48; not v1 is isolated by Th1; then v1.edgesInOut() <> {} by GLIB_000:def 49; then 0 < card v1.edgesInOut() by NAT_1:3; then A7: 0+1 <= card v1.edgesInOut() by NAT_1:13; Gkb is connected by A5,Lm20; then k <= Gk1.size() - card v1.edgesInOut() + 1 by A2,A6; then k+1 <= Gk1.size() + 1 - card v1.edgesInOut() + card v1 .edgesInOut() by A7,XREAL_1:7; hence Gk1.order() <= Gk1.size() + 1 by A3; end; hence P[Gk1]; end; A8: for G being finite _Graph st G.order() = 1 holds P[G] by NAT_1:12; for G being finite _Graph holds P[G] from GLIB_000:sch 1(A8,A1); hence thesis; end; theorem for G being acyclic _Graph holds G is simple; theorem 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 by Lm22; theorem 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) by Lm23; theorem Th43: G1 == G2 & G1 is acyclic implies G2 is acyclic proof assume that A1: G1 == G2 and A2: G1 is acyclic; reconsider G19 = G1 as acyclic _Graph by A2; G2 is Subgraph of G19 by A1,GLIB_000:87; hence thesis; end; theorem 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 by Lm24; theorem Th45: for G being finite _Graph holds G is Tree-like iff G is acyclic & G.order() = G.size() + 1 proof defpred P[Nat] means for G being finite acyclic _Graph st G.order() = $1 & G .order() = G.size() + 1 holds G is connected; let G be finite _Graph; hereby defpred P[Nat] means for T being finite Tree-like _Graph st T.order() = $1 holds $1 = T.size() + 1; assume A1: G is Tree-like; hence G is acyclic; now let T be finite Tree-like _Graph; set VT = the_Vertices_of T, ET = the_Edges_of T; assume T.order() = 1; then card VT = 1 by GLIB_000:def 24; then consider v being object such that A2: VT = {v} by CARD_2:42; reconsider v as Vertex of T by A2,TARSKI:def 1; now given e being object such that A3: e in ET; (the_Target_of T).e in {v} by A2,A3,FUNCT_2:5; then A4: (the_Target_of T).e = v by TARSKI:def 1; (the_Source_of T).e in {v} by A2,A3,FUNCT_2:5; then (the_Source_of T).e = v by TARSKI:def 1; then e Joins v,v,T by A3,A4,GLIB_000:def 13; then T.walkOf(v,e,v) is Cycle-like by GLIB_001:156; hence contradiction by Def2; end; then card ET = 0 by CARD_1:27,XBOOLE_0:def 1; then T.size() = 0 by GLIB_000:def 25; hence 1 = T.size() + 1; end; then A5: P[1]; now let k be non zero Nat; assume A6: for T being finite Tree-like _Graph st T.order() = k holds k = T.size() + 1; let T be finite Tree-like _Graph; assume A7: T.order() = k+1; then T.order() <> 1 by XCMPLX_1:3; then reconsider aT = T as non trivial finite Tree-like _Graph by GLIB_000:26; set v = the endvertex Vertex of aT; set T2 = the removeVertex of aT,v; T2.order() + 1 - 1 = k + 1 - 1 by A7,GLIB_000:48; then A8: k = T2.size() + 1 by A6; card v.edgesInOut() = v.degree() by GLIB_000:19 .= 1 by GLIB_000:def 52; hence k+1 = T.size() + 1 by A8,GLIB_000:48; end; then A9: for k being non zero Nat st P[k] holds P[k+1]; for k being non zero Nat holds P[k] from NAT_1:sch 10(A5,A9); hence G.order() = G.size() + 1 by A1; end; assume that A10: G is acyclic and A11: G.order() = G.size() + 1; now let k be non zero Element of NAT; assume A12: for G being finite acyclic _Graph st G.order() = k & G.order() = G.size() + 1 holds G is connected; let G be finite acyclic _Graph; assume that A13: G.order() = k+1 and A14: G.order() = G.size()+1; now assume G.order() = 1; then 0 + 1 = k + 1 by A13; hence contradiction; end; then reconsider aG = G as non trivial finite acyclic _Graph by GLIB_000:26; the_Edges_of G <> {} by A13,A14,CARD_1:27,GLIB_000:def 25; then consider v,v2 being Vertex of aG such that v <> v2 and A15: v is endvertex and v2 is endvertex and v2 in aG.reachableFrom(v) by Lm23; set G2 = the removeVertex of G,v; A16: G2.order() + 1 = aG.order() & G2.size() + card v.edgesInOut() = aG .size() by GLIB_000:48; card v.edgesInOut() = v.degree() by GLIB_000:19 .= 1 by A15,GLIB_000:def 52; then A17: G2 is connected by A12,A13,A14,A16; consider e being object such that A18: v.edgesInOut() = {e} and A19: not e Joins v,v,G by A15,GLIB_000:def 51; e in v.edgesInOut() by A18,TARSKI:def 1; hence G is connected by A17,A19,Th2; end; then A20: for k being non zero Nat st P[k] holds P[k+1]; now let G be finite acyclic _Graph; assume that A21: G.order() = 1 and G.order() = G.size() + 1; consider v being Vertex of G such that A22: the_Vertices_of G = {v} by A21,GLIB_000:27; now let v1,v2 be Vertex of G; v1 = v & v2 = v by A22,TARSKI:def 1; then G.walkOf(v) is_Walk_from v1,v2 by GLIB_001:13; hence ex W being Walk of G st W is_Walk_from v1,v2; end; hence G is connected; end; then A23: P[1]; for k being non zero Nat holds P[k] from NAT_1:sch 10(A23,A20); then G is connected by A10,A11; hence thesis by A10; end; theorem for G being finite _Graph holds G is Tree-like iff G is connected & G .order() = G.size() + 1 proof let G be finite _Graph; thus G is Tree-like implies G is connected & G.order() = G.size()+1 by Th45; assume that A1: G is connected and A2: G.order() = G.size() + 1; now assume not G is acyclic; then consider W being Walk of G such that A3: W is Cycle-like; set e = the Element of W.edges(); set G2 = the removeEdge of G,e; A4: W.edges() <> {} by A3,GLIB_001:136; then e in W.edges(); then A5: G2.order()=G.order() & G2.size()+1=G.size() by GLIB_000:52; G2 is connected by A1,A3,A4,Th4; then G2.size() + 1 + 1 <= G2.size() + 1 + 0 by A2,A5,Th39; hence contradiction by XREAL_1:6; end; hence thesis by A1; end; theorem Th47: G1 == G2 & G1 is Tree-like implies G2 is Tree-like by Th7,Th43; theorem G is_DTree_rooted_at x implies x is Vertex of G proof set v = the Vertex of G; assume G is_DTree_rooted_at x; then ex W being DWalk of G st W is_Walk_from x,v; hence thesis by GLIB_001:18; end; theorem G1 == G2 & G1 is_DTree_rooted_at x implies G2 is_DTree_rooted_at x proof assume that A1: G1 == G2 and A2: G1 is_DTree_rooted_at x; A3: now let y be Vertex of G2; reconsider y9 = y as Vertex of G1 by A1,GLIB_000:def 34; consider W being DWalk of G1 such that A4: W is_Walk_from x,y9 by A2; reconsider W9=W as DWalk of G2 by A1,GLIB_001:179,181; take W9; thus W9 is_Walk_from x,y by A4,GLIB_001:19; end; G1 is Tree-like by A2; then G2 is Tree-like by A1,Th47; hence thesis by A3; end;