:: About Supergraphs, Part {I} :: by Sebastian Koch :: :: Received June 29, 2018 :: Copyright (c) 2018-2021 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, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ORDINAL4, ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE, FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, FUNCOP_1, TREES_1, GLIB_001, FUNCT_4, GLIB_006, ABIAN, REWRITE1, CHORD, RCOMP_1, WAYBEL_0, FINSEQ_8, GRAPH_1, JORDAN3, RFINSEQ, XCMPLX_0, INT_1, MSAFREE2, CARD_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, RVSUM_1, RFINSEQ, FUNCT_7, ABIAN, FINSEQ_6, GLIB_000, FINSEQ_8, GRAPH_2, GRAPH_5, GLIB_001, GLIB_002, CHORD; constructors DOMAIN_1, BINOP_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5, ABIAN, WELLORD2, FUNCT_2, FIB_NUM2, FINSEQ_8, GLIB_001, GLIB_002, RELSET_1, FUNCT_3, CHORD, NAT_D, GRAPH_2, RFINSEQ, FINSEQ_6, CARD_2, FUNCT_7, FINSEQ_1, SUBSET_1; registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSET_1, ABIAN, XREAL_0, NAT_1, FINSEQ_1, GLIB_000, GLIB_001, HELLY, GLIB_002, CHORD, INT_1, CARD_1, HURWITZ2, RELSET_1, RAMSEY_1; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: general preliminaries :: into ABIAN ? theorem :: GLIB_006:1 for n being even Integer, m being odd Integer st n <= m holds n+1 <= m; :: into ABIAN ? theorem :: GLIB_006:2 for n being even Integer, m being odd Integer st m <= n holds m+1 <= n; :: into NAT_D ? theorem :: GLIB_006:3 for i, j being Nat st i > i -' 1 + j holds j = 0; :: BEGIN into FINSEQ_6 or JORDAN4 ? theorem :: GLIB_006:4 for f, g being FinSequence, i being Nat st i <= len f & mid(f,i,i-'1+len g) = g holds i-'1+len g <= len f; theorem :: GLIB_006:5 for p being FinSequence, n being Nat st n in dom p & n+1 <= len p holds mid(p,n,n+1) = <*p.n, p.(n+1)*>; theorem :: GLIB_006:6 for p being FinSequence, n being Nat st n in dom p & n+2 <= len p holds mid(p,n,n+2) = <*p.n, p.(n+1),p.(n+2)*>; :: END into FINSEQ_6 or JORDAN 4 ? :: during research the author noticed the strong similiariy between :: (m,n)-cut p and smid(p,m,n) (from GRAPH_2 and FINSEQ_8) :: but no theorems about that will be made here :: SOLVED: added theorem at the end of FINSEQ_8 :: BEGIN into FINSEQ_8 ? theorem :: GLIB_006:7 for D being non empty set, f,g being FinSequence of D, n being Nat st g is_substring_of f,n holds len g = 0 or (1 <= n-'1+len g & n-'1+len g <= len f & n <= n-'1+len g); definition let D be non empty set, f,g be FinSequence of D, n be Nat; pred g is_odd_substring_of f,n means :: GLIB_006:def 1 len g > 0 implies ex i being odd Nat st n <= i & i <= len f & mid(f,i,(i-'1)+len g) = g; pred g is_even_substring_of f,n means :: GLIB_006:def 2 len g > 0 implies ex i being even Nat st n <= i & i <= len f & mid(f,i,(i-'1)+len g) = g; end; theorem :: GLIB_006:8 for D being non empty set, f,g being FinSequence of D, n being Nat holds g is_odd_substring_of f,n implies g is_substring_of f,n; theorem :: GLIB_006:9 for D being non empty set, f,g being FinSequence of D, n being Nat holds g is_even_substring_of f,n implies g is_substring_of f,n; theorem :: GLIB_006:10 for D being non empty set, f,g being FinSequence of D, n,m being Nat st m >= n holds (g is_odd_substring_of f,m implies g is_odd_substring_of f,n) & (g is_even_substring_of f,m implies g is_even_substring_of f,n); theorem :: GLIB_006:11 for D being non empty set, f being FinSequence of D st 1 <= len f holds f is_odd_substring_of f,0; theorem :: GLIB_006:12 for D being non empty set, f,g being FinSequence of D, n being even Element of NAT st g is_odd_substring_of f,n holds g is_odd_substring_of f,n+1; theorem :: GLIB_006:13 for D being non empty set, f,g being FinSequence of D, n being odd Element of NAT st g is_even_substring_of f,n holds g is_even_substring_of f,n+1; theorem :: GLIB_006:14 for D being non empty set, f,g being FinSequence of D st g is_odd_substring_of f,0 holds g is_odd_substring_of f,1; :: There are plenty theorems regarding predicate is_substring_of and :: its even/odd equivalents that could be written here. :: Many of them regard if the predicate holds with certain FinSequence :: functors, e.g. :: theorem for D being non empty set, f being FinSequence of D, m,n being Nat :: st 1 <= m & m <= n & n <= len f holds (m,n)-cut p is_substring_of p,m :: theorem for D being non empty set, f being FinSequence of D, m,n being Nat :: holds (m,n)-cut p is_substring_of p,0 :: However, these theorems will not be proven here. Another set of theorems :: deals with the transitivity properties of the predicate, e.g. :: theorem for D being non empty set, f,g,h being FinSequence of D, :: n,m being Element of NAT :: st g is_substring_of f,n & h is_substring_of g,m :: holds h is_substring_of f,n+m-'1 :: theorem for D being non empty set, f,g,h being FinSequence of D, :: n,m being Element of NAT :: st g is_even_substring_of f,n & h is_even_substring_of g,m :: holds h is_odd_substring_of f,n+m-'1 :: These theorems will not be further investigated here either. :: However, the author proposes the writing of an article that :: deals with these properties along with the aforementioned :: -cut/smid similiarity (maybe as FINSEQ_9 or add it to FINSEQ_8). :: END into FINSEQ_8 ? begin :: graph preliminaries :: into GLIB_000 ? registration let G be non-Dmulti _Graph; cluster -> non-Dmulti for Subgraph of G; end; :: into GLIB_000 ? theorem :: GLIB_006:15 for G being _Graph holds G is inducedSubgraph of G, the_Vertices_of G; :: into GLIB_000 ? theorem :: GLIB_006:16 for G1,G3 being _Graph, V,E being set, G2 being inducedSubgraph of G1,V,E st G2 == G3 holds G3 is inducedSubgraph of G1,V,E; :: into GLIB_000 ? theorem :: GLIB_006:17 for G being _Graph, X being set, e,y being object st e SJoins X,{y},G ex x being object st x in X & e Joins x,y,G; :: into GLIB_000 ? theorem :: GLIB_006:18 for G being _Graph, X being set st X /\ the_Vertices_of G = {} holds G.edgesInto(X) = {} & G.edgesOutOf(X) = {} & G.edgesInOut(X) = {} & G.edgesBetween(X) = {}; :: into GLIB_000 ? theorem :: GLIB_006:19 for G being _Graph, X1, X2 being set, y being object st X1 misses X2 holds G.edgesBetween(X1,{y}) misses G.edgesBetween(X2,{y}); :: into GLIB_000 ? theorem :: GLIB_006:20 for G being _Graph, X1, X2 being set, y being object holds G.edgesBetween(X1 \/ X2,{y}) = G.edgesBetween(X1,{y}) \/ G.edgesBetween(X2,{y}); :: into GLIB_000 ? :: generalization of GLIB_000:22, uses it for simplification of proof theorem :: GLIB_006:21 for G being _trivial _Graph ex v being Vertex of G st the_Vertices_of G = {v} & the_Source_of G = the_Edges_of G --> v & the_Target_of G = the_Edges_of G --> v; :: definitely into GLIB_001 registration let G be _Graph; cluster closed Trail-like non trivial -> Circuit-like for Walk of G; cluster closed Path-like non trivial -> Cycle-like for Walk of G; end; :: generalizes part of GLIB_001:175 and GLIB_001:176 :: into GLIB_001 ? theorem :: GLIB_006:22 for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 is Trail-like implies W2 is Trail-like; :: generalizes part of GLIB_001:175 and GLIB_001:176 :: into GLIB_001 ? theorem :: GLIB_006:23 for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 is Path-like implies W2 is Path-like; :: generalizes part of GLIB_001:175 and GLIB_001:176 :: more general version of CHORD:24 :: into GLIB_001 ? theorem :: GLIB_006:24 for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 is Cycle-like implies W2 is Cycle-like; :: generalizes part of GLIB_001:175 and GLIB_001:176 :: into GLIB_001 ? theorem :: GLIB_006:25 for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 is vertex-distinct implies W2 is vertex-distinct; :: BEGIN into GLIB_001 ? :: Four theorems have been left out, as they need more theorems :: about is_substring_of (and the even/odd equivalents), :: and that is not part of this article. :: The theorems left out here are: :: theorem for G being _Graph, W being Walk of G, m,n being odd Nat, :: m2 being Element of NAT :: st m <= n & n <= len W & m = m2 holds W.cut(m,n) is_odd_substring_of W,m2 :: theorem for G being _Graph, W being Walk of G, m,n being Nat holds :: W.cut(m,n) is_odd_substring_of W,0 :: theorem for G being _Graph, W1, W2 being Walk of G st W1.last() = W2.first() :: holds W2 is_odd_substring_of W1.append(W2),len W1 :: theorem for G being _Graph, W1, W2 being Walk of G :: holds W1 is_odd_substring_of W1.append(W2),0 theorem :: GLIB_006:26 for G being _Graph, W being Walk of G, v being Vertex of G st v in W.vertices() holds G.walkOf(v) is_substring_of W, 0; theorem :: GLIB_006:27 for G being _Graph, W being Walk of G, n being odd Element of NAT st n+2 <= len W holds G.walkOf(W.n,W.(n+1),W.(n+2)) is_odd_substring_of W, 0; theorem :: GLIB_006:28 for G being _Graph, W being Walk of G, u,e,v being object st e Joins u,v,G & e in W.edges() holds G.walkOf(u,e,v) is_odd_substring_of W, 0 or G.walkOf(v,e,u) is_odd_substring_of W, 0; theorem :: GLIB_006:29 for G being _Graph, W being Walk of G, u,e,v being object st e Joins u,v,G & G.walkOf(u,e,v) is_odd_substring_of W, 0 holds e in W.edges() & u in W.vertices() & v in W.vertices(); definition let G be _Graph, W1, W2 be Walk of G; func W1.findFirstVertex(W2) -> odd Element of NAT means :: GLIB_006:def 3 it <= len W1 & ex k being even Nat st it = k+1 & (for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n) = W2.n) & for l being even Nat st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n holds k <= l if W2 is_odd_substring_of W1, 0 otherwise it = len W1; func W1.findLastVertex(W2) -> odd Element of NAT means :: GLIB_006:def 4 it <= len W1 & ex k being even Nat st it = k+len W2 & (for n being Nat st 1 <= n & n <= len W2 holds W1.(k+n) = W2.n) & for l being even Nat st for n being Nat st 1 <= n & n <= len W2 holds W1.(l+n) = W2.n holds k <= l if W2 is_odd_substring_of W1, 0 otherwise it = len W1; end; theorem :: GLIB_006:30 for G being _Graph, W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds W1.(W1.findFirstVertex(W2)) = W2.first() & W1.(W1.findLastVertex(W2)) = W2.last(); theorem :: GLIB_006:31 for G being _Graph, W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds 1 <= W1.findFirstVertex(W2) & W1.findFirstVertex(W2) <= len W1 & 1 <= W1.findLastVertex(W2) & W1.findLastVertex(W2) <= len W1; theorem :: GLIB_006:32 for G being _Graph, W being Walk of G holds 1 = W.findFirstVertex(W) & W.findLastVertex(W) = len W; theorem :: GLIB_006:33 for G being _Graph, W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds W1.findFirstVertex(W2) <= W1.findLastVertex(W2); definition let G be _Graph, W1, W2, W3 be Walk of G; func W1.replaceWith(W2, W3) -> Walk of G equals :: GLIB_006:def 5 W1.cut(1,W1.findFirstVertex(W2) ).append(W3 ).append(W1.cut(W1.findLastVertex(W2), len W1)) if W2 is_odd_substring_of W1, 0 & W2.first() = W3.first() & W2.last() = W3.last() otherwise W1; end; definition let G be _Graph, W1, W3 be Walk of G; let e be object; func W1.replaceEdgeWith(e, W3) -> Walk of G equals :: GLIB_006:def 6 W1.replaceWith(G.walkOf(W3.first(),e,W3.last()),W3) if e Joins W3.first(),W3.last(),G & G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0 otherwise W1; end; definition let G be _Graph, W1, W2 be Walk of G; let e be object; func W1.replaceWithEdge(W2, e) -> Walk of G equals :: GLIB_006:def 7 W1.replaceWith(W2,G.walkOf(W2.first(),e,W2.last())) if W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G otherwise W1; end; theorem :: GLIB_006:34 for G being _Graph, W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2.first() = W3.first() & W2.last() = W3.last() holds W1.cut(1,W1.findFirstVertex(W2)).first() = W1.first() & W1.cut(1,W1.findFirstVertex(W2)).last() = W3.first() & W1.cut(1,W1.findFirstVertex(W2)).append(W3).first() = W1.first() & W1.cut(1,W1.findFirstVertex(W2)).append(W3).last() = W3.last() & W1.cut(W1.findLastVertex(W2), len W1).first() = W3.last() & W1.cut(W1.findLastVertex(W2), len W1).last() = W1.last(); theorem :: GLIB_006:35 for G being _Graph, W1, W2, W3 being Walk of G holds W1.first() = W1.replaceWith(W2, W3).first() & W1.last() = W1.replaceWith(W2, W3).last(); theorem :: GLIB_006:36 for G being _Graph, W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2.first() = W3.first() & W2.last() = W3.last() holds W1.replaceWith(W2, W3).vertices() = W1.cut(1,W1.findFirstVertex(W2)).vertices() \/ W3.vertices() \/ W1.cut(W1.findLastVertex(W2), len W1).vertices(); theorem :: GLIB_006:37 for G being _Graph, W1, W2, W3 being Walk of G st W2 is_odd_substring_of W1, 0 & W2.first() = W3.first() & W2.last() = W3.last() holds W1.replaceWith(W2, W3).edges() = W1.cut(1,W1.findFirstVertex(W2)).edges() \/ W3.edges() \/ W1.cut(W1.findLastVertex(W2), len W1).edges(); theorem :: GLIB_006:38 for G being _Graph, W1, W3 being Walk of G, e being object st e Joins W3.first(),W3.last(),G & G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0 holds e in W1.replaceEdgeWith(e, W3).edges() iff e in W1.cut(1,W1.findFirstVertex(G.walkOf(W3.first(),e,W3.last()))).edges() or e in W3.edges() or e in W1.cut(W1.findLastVertex( G.walkOf(W3.first(),e,W3.last())), len W1).edges(); :: The Proof got surprisingly long. Maybe there's a shorter way? theorem :: GLIB_006:39 for G being _Graph, W1, W3 being Walk of G, e being object st e Joins W3.first(),W3.last(),G & not e in W3.edges() & G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0 & for n, m being even Nat st n in dom W1 & m in dom W1 & W1.n = e & W1.m = e holds n = m holds not e in W1.replaceEdgeWith(e, W3).edges(); :: this is the important theorem from this whole preliminary theory :: on replacement of parts of walks that will be used in the main part theorem :: GLIB_006:40 for G being _Graph, T1 being Trail of G, W3 being Walk of G, e being object st e Joins W3.first(),W3.last(),G & not e in W3.edges() & G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of T1, 0 holds not e in T1.replaceEdgeWith(e, W3).edges(); theorem :: GLIB_006:41 for G being _Graph, W1, W2 being Walk of G st W1.first() = W2.first() & W1.last() = W2.last() holds W1.replaceWith(W1,W2) = W2; :: The following theorem has been left out :: theorem ThExtra: for G being _Graph, W1, W2 being Walk of G :: holds W1.replaceWith(W2,W2) = W1 :: as it needs :: theorem for G being _Graph, W1, W2 being Walk of G :: st W2 is_odd_substring_of W1,0 holds ex m,n being Element of NAT :: st 1 <= m & m <= n & n <= len W2 & W1.cut(m,n) = W2 :: which in turn relies on unproven theorems about is_odd_substring_of :: and -cut/smid. :: the assumption in the following theorem could be dropped :: if the theorems above would be available theorem :: GLIB_006:42 for G being _Graph, W1, W3 being Walk of G, e being object st e Joins W3.first(),W3.last(),G & G.walkOf(W3.first(),e,W3.last()) is_odd_substring_of W1, 0 holds ex W2 being Walk of G st W1.replaceEdgeWith(e,W3) = W1.replaceWith(W2,W3); :: same as theorem above theorem :: GLIB_006:43 for G being _Graph, W1, W2 being Walk of G, e being object st W2 is_odd_substring_of W1, 0 & e Joins W2.first(),W2.last(),G holds ex W3 being Walk of G st W1.replaceWithEdge(W2,e) = W1.replaceWith(W2,W3); theorem :: GLIB_006:44 for G being _Graph, W1, W3 being Walk of G, e being object holds W1.first() = W1.replaceEdgeWith(e, W3).first() & W1.last() = W1.replaceEdgeWith(e, W3).last(); theorem :: GLIB_006:45 for G being _Graph, W1, W2 being Walk of G, e being object holds W1.first() = W1.replaceWithEdge(W2, e).first() & W1.last() = W1.replaceWithEdge(W2, e).last(); theorem :: GLIB_006:46 for G being _Graph, W1, W2, W3 being Walk of G, u,v being object holds W1 is_Walk_from u,v iff W1.replaceWith(W2, W3) is_Walk_from u,v; theorem :: GLIB_006:47 for G being _Graph, W1, W3 being Walk of G, e,u,v being object holds W1 is_Walk_from u,v iff W1.replaceEdgeWith(e, W3) is_Walk_from u,v; theorem :: GLIB_006:48 for G being _Graph, W1, W2 being Walk of G, e,u,v being object holds W1 is_Walk_from u,v iff W1.replaceWithEdge(W2, e) is_Walk_from u,v; :: END into GLIB_001 ? :: into GLIB_002 ? theorem :: GLIB_006:49 for G being _Graph, v1, v2 being Vertex of G st v1 is isolated & v1 <> v2 holds not v2 in G.reachableFrom v1; :: into GLIB_002 ? theorem :: GLIB_006:50 for G being _Graph, v1, v2 being Vertex of G holds v1 in G.reachableFrom v2 implies v2 in G.reachableFrom v1; :: into GLIB_002 ? theorem :: GLIB_006:51 for G being _Graph, v being Vertex of G st v is isolated holds {v} = G.reachableFrom(v); :: into GLIB_002 ? theorem :: GLIB_006:52 for G being _Graph, v being Vertex of G, C being inducedSubgraph of G, {v} st v is isolated holds C is Component of G; :: into GLIB_002 ? theorem :: GLIB_006:53 for G1 being non _trivial _Graph, v being Vertex of G1, G2 being removeVertex of G1, v st v is isolated holds G1.componentSet() = G2.componentSet() \/ {{v}} & G1.numComponents() = G2.numComponents() +` 1; :: into GLIB_002 ? registration let G be _Graph; cluster isolated -> non cut-vertex for Vertex of G; end; :: into GLIB_002 ? theorem :: GLIB_006:54 for G1 being _Graph, G2 being Subgraph of G1, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1 is Cycle-like iff W2 is Cycle-like; :: into GLIB_002 ? theorem :: GLIB_006:55 for G1 being connected _Graph, G2 being Component of G1 holds G1 == G2; :: into CHORD ? registration cluster complete -> connected for _Graph; end; registration cluster non non-Dmulti non non-multi non loopless non Dsimple non simple non acyclic non _finite for _Graph; end; reserve G for _Graph; definition let G; func Endvertices(G) -> Subset of the_Vertices_of G means :: GLIB_006:def 8 for v being object holds v in it iff ex w being Vertex of G st v = w & w is endvertex; end; theorem :: GLIB_006:56 for v being Vertex of G holds v in Endvertices(G) iff v is endvertex; begin :: Supergraphs :: analogue to GLIB_000:def 32 definition let G; mode Supergraph of G -> _Graph means :: GLIB_006:def 9 the_Vertices_of G c= the_Vertices_of it & the_Edges_of G c= the_Edges_of it & for e being set st e in the_Edges_of G holds (the_Source_of G).e = (the_Source_of it).e & (the_Target_of G).e = (the_Target_of it).e; end; :: Now we show some handy trivialities. Most of them have a :: Subgraph equivalent in e.g. GLIB_000 and are shown through it and :: the following theorem :: Hence not all Subgraph theorems are reproduced here as they can be easily :: shown. theorem :: GLIB_006:57 for G1, G2 being _Graph holds G2 is Subgraph of G1 iff G1 is Supergraph of G2; theorem :: GLIB_006:58 for G1, G2 being _Graph holds G2 is Subgraph of G1 & G2 is Supergraph of G1 iff G1 == G2; theorem :: GLIB_006:59 for G1, G2 being _Graph holds G1 is Supergraph of G2 & G2 is Supergraph of G1 iff G1 == G2; theorem :: GLIB_006:60 for G1, G2 being _Graph holds G1 is Supergraph of G2 iff G2 c= G1; theorem :: GLIB_006:61 G is Supergraph of G; theorem :: GLIB_006:62 for G3 being _Graph, G2 being Supergraph of G3, G1 being Supergraph of G2 holds G1 is Supergraph of G3; reserve G2 for _Graph, G1 for Supergraph of G2; :: the following 4 Supergraph theorems have no Subgraph analogon in the MML yet theorem :: GLIB_006:63 for G1, G2 being _Graph st the_Vertices_of G2 c= the_Vertices_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 holds G1 is Supergraph of G2; theorem :: GLIB_006:64 for G2, G1 holds the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1; theorem :: GLIB_006:65 for G2, G1 st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 holds G1 == G2; theorem :: GLIB_006:66 for G1, G2 being _Graph st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 holds G1 == G2; theorem :: GLIB_006:67 for G2, G1 for x being set holds (x in the_Vertices_of G2 implies x in the_Vertices_of G1) & (x in the_Edges_of G2 implies x in the_Edges_of G1); theorem :: GLIB_006:68 for G2, G1 for v being Vertex of G2 holds v is Vertex of G1; theorem :: GLIB_006:69 for G2, G1 holds the_Source_of G2 = (the_Source_of G1) | the_Edges_of G2 & the_Target_of G2 = (the_Target_of G1) | the_Edges_of G2; theorem :: GLIB_006:70 for G2, G1 for x,y being set, e being object holds (e Joins x,y,G2 implies e Joins x,y,G1) & (e DJoins x,y,G2 implies e DJoins x,y,G1) & (e SJoins x,y,G2 implies e SJoins x,y,G1) & (e DSJoins x,y,G2 implies e DSJoins x,y,G1); theorem :: GLIB_006:71 for G2, G1 for e,v1,v2 being object st e DJoins v1,v2,G1 holds e DJoins v1,v2,G2 or not e in the_Edges_of G2; theorem :: GLIB_006:72 for G2, G1 for e,v1,v2 being object st e Joins v1,v2,G1 holds e Joins v1,v2,G2 or not e in the_Edges_of G2; registration let G be _finite _Graph; cluster _finite for Supergraph of G; end; :: no equivalent in GLIB_000 theorem :: GLIB_006:73 for G2, G1 holds G2.order() c= G1.order() & G2.size() c= G1.size(); theorem :: GLIB_006:74 for G2 being _finite _Graph, G1 being _finite Supergraph of G2 holds G2.order() <= G1.order() & G2.size() <= G1.size(); theorem :: GLIB_006:75 for G2, G1 for W being Walk of G2 holds W is Walk of G1; theorem :: GLIB_006:76 for G2, G1 for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2 holds (W1 is closed iff W2 is closed) & (W1 is directed iff W2 is directed) & (W1 is trivial iff W2 is trivial) & (W1 is Trail-like iff W2 is Trail-like) & (W1 is Path-like iff W2 is Path-like) & (W1 is vertex-distinct iff W2 is vertex-distinct) & (W1 is Cycle-like iff W2 is Cycle-like); registration let G be non _trivial _Graph; cluster -> non _trivial for Supergraph of G; end; registration let G be non non-Dmulti _Graph; cluster -> non non-Dmulti for Supergraph of G; end; registration let G be non non-multi _Graph; cluster -> non non-multi for Supergraph of G; end; registration let G be non loopless _Graph; cluster -> non loopless for Supergraph of G; end; registration let G be non Dsimple _Graph; cluster -> non Dsimple for Supergraph of G; end; registration let G be non simple _Graph; cluster -> non simple for Supergraph of G; end; registration let G be non acyclic _Graph; cluster -> non acyclic for Supergraph of G; end; registration let G be non _finite _Graph; cluster -> non _finite for Supergraph of G; end; reserve V for set; definition let G, V; mode addVertices of G, V -> Supergraph of G means :: GLIB_006:def 10 the_Vertices_of it = the_Vertices_of G \/ V & the_Edges_of it = the_Edges_of G & the_Source_of it = the_Source_of G & the_Target_of it = the_Target_of G; end; theorem :: GLIB_006:77 for G, V for G1, G2 being addVertices of G, V holds G1 == G2; theorem :: GLIB_006:78 for G2, V for G1 being addVertices of G2, V holds G1 == G2 iff V c= the_Vertices_of G2; theorem :: GLIB_006:79 for G1, G2 being _Graph, V being set st G1 == G2 & V c= the_Vertices_of G2 holds G1 is addVertices of G2, V; theorem :: GLIB_006:80 for G, G2, V for G1 being addVertices of G, V st G1 == G2 holds G2 is addVertices of G, V; theorem :: GLIB_006:81 for G2, V for G1 being addVertices of G2, V holds G1.edgesBetween(the_Vertices_of G2) = the_Edges_of G1; theorem :: GLIB_006:82 for G3 being _Graph, V1, V2 being set, G2 being addVertices of G3, V2, G1 being addVertices of G2, V1 holds G1 is addVertices of G3, V1 \/ V2; theorem :: GLIB_006:83 for G3 being _Graph, V1, V2 being set, G1 being addVertices of G3, V1 \/ V2 holds ex G2 being addVertices of G3, V2 st G1 is addVertices of G2, V1; theorem :: GLIB_006:84 for G2, V for G1 being addVertices of G2, V holds G2 is inducedSubgraph of G1, the_Vertices_of G2; theorem :: GLIB_006:85 for G2, V for G1 being addVertices of G2, V for x,y,e being object holds e DJoins x,y,G1 iff e DJoins x,y,G2; theorem :: GLIB_006:86 for G2, V for G1 being addVertices of G2, V, v being object st v in V holds v is Vertex of G1; theorem :: GLIB_006:87 for G2, V for G1 being addVertices of G2, V for x,y,e being object holds e Joins x,y,G1 iff e Joins x,y,G2; theorem :: GLIB_006:88 for G2, V for G1 being addVertices of G2, V, v being Vertex of G1 st v in V \ the_Vertices_of G2 holds v is isolated non cut-vertex; theorem :: GLIB_006:89 for G2, V for G1 being addVertices of G2, V st V \ the_Vertices_of G2 <> {} holds G1 is non _trivial non connected non Tree-like non complete; registration let G be non-Dmulti _Graph; let V be set; cluster -> non-Dmulti for addVertices of G, V; end; registration let G be non-multi _Graph; let V be set; cluster -> non-multi for addVertices of G, V; end; registration let G be loopless _Graph; let V be set; cluster -> loopless for addVertices of G, V; end; registration let G be Dsimple _Graph; let V be set; cluster -> Dsimple for addVertices of G, V; end; registration let G be Dsimple _Graph; let V be set; cluster -> Dsimple for addVertices of G, V; end; theorem :: GLIB_006:90 for G2, V for G1 being addVertices of G2, V, W being Walk of G1 holds W.vertices() misses V \ the_Vertices_of G2 or W is trivial; theorem :: GLIB_006:91 for G2, V for G1 being addVertices of G2, V, W being Walk of G1 st W.vertices() misses V \ the_Vertices_of G2 holds W is Walk of G2; registration let G be acyclic _Graph; let V be set; cluster -> acyclic for addVertices of G, V; end; theorem :: GLIB_006:92 for G2, V for G1 being addVertices of G2, V holds G2 is chordal iff G1 is chordal; :: "non"-version of this cluster has to wait :: because non chordal existence will be proven with cycle graphs registration let G be chordal _Graph; let V be set; cluster -> chordal for addVertices of G, V; end; reserve v for object; definition let G, v; mode addVertex of G, v is addVertices of G, {v}; end; theorem :: GLIB_006:93 for G2, v for G1 being addVertex of G2, v holds G1 == G2 iff v in the_Vertices_of G2; theorem :: GLIB_006:94 for G2, v for G1 being addVertex of G2, v holds v is Vertex of G1; registration let G; cluster -> non _trivial non connected non complete for addVertex of G, the_Vertices_of G; end; :: the prime example of how to use the new modes to show existences :: of certain graphs registration cluster non _trivial non connected non complete for _Graph; end; registration let G be non connected _Graph, V be set; cluster -> non connected for addVertices of G, V; end; :: In general, non finite versions of cardinalities are missing in the :: graph construction modes of GLIB_000 (e.g. removeVertex) and should :: be added. theorem :: GLIB_006:95 for G2, V for G1 being addVertices of G2, V holds G1.size() = G2.size() & G1.order() = G2.order() +` card (V \ the_Vertices_of G2); theorem :: GLIB_006:96 for G2 being _finite _Graph, V being finite set, G1 being addVertices of G2,V holds G1.order() = G2.order() + card (V \ the_Vertices_of G2); theorem :: GLIB_006:97 for G2 being _Graph, v being object, G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds G1.order() = G2.order() +` 1; theorem :: GLIB_006:98 for G2 being _finite _Graph, v being object, G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds G1.order() = G2.order() + 1; registration let G be _finite _Graph, V be finite set; cluster -> _finite for addVertices of G, V; end; registration let G be _finite _Graph, v be object; cluster -> _finite for addVertex of G, v; end; registration let G be _Graph, V be non finite set; cluster -> non _finite for addVertices of G,V; end; :: we explicitly add an edge only if it is not used already :: to ensure getting a Supergraph definition let G; let v1,e,v2 be object; mode addEdge of G,v1,e,v2 -> Supergraph of G means :: GLIB_006:def 11 the_Vertices_of it = the_Vertices_of G & the_Edges_of it = the_Edges_of G \/ {e} & the_Source_of it = the_Source_of G +* (e .--> v1) & the_Target_of it = the_Target_of G +* (e .--> v2) if v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G otherwise it == G; end; theorem :: GLIB_006:99 for G for v1,e,v2 being object, G1, G2 being addEdge of G,v1,e,v2 holds G1 == G2; theorem :: GLIB_006:100 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 holds G1 == G2 iff e in the_Edges_of G2; theorem :: GLIB_006:101 for G, G2 for v1,e,v2 being object, G1 being addEdge of G,v1,e,v2 st G1 == G2 holds G2 is addEdge of G,v1,e,v2; theorem :: GLIB_006:102 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 holds the_Vertices_of G1 = the_Vertices_of G2; theorem :: GLIB_006:103 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 holds G1.edgesBetween(the_Vertices_of G2) = the_Edges_of G1; theorem :: GLIB_006:104 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 for v being Vertex of G1 holds v is Vertex of G2; theorem :: GLIB_006:105 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 holds not e in the_Edges_of G2 implies e DJoins v1,v2,G1; theorem :: GLIB_006:106 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 for e1,w1,w2 being object holds e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 implies e1 = e; theorem :: GLIB_006:107 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 for e1,w1,w2 being object holds e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 implies (w1 = v1 & w2 = v2) or (w1 = v2 & w2 = v1); theorem :: GLIB_006:108 for G2 for v1, v2 being Vertex of G2, e being set for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds G2 is removeEdge of G1,e; theorem :: GLIB_006:109 for G2 for v1, v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2, W being Walk of G1 st (e in W.edges() implies e in the_Edges_of G2) holds W is Walk of G2; registration let G be _trivial _Graph; let v1,e,v2 be object; cluster -> _trivial for addEdge of G,v1,e,v2; end; registration let G be connected _Graph; let v1,e,v2 be object; cluster -> connected for addEdge of G,v1,e,v2; end; registration let G be complete _Graph; let v1,e,v2 be object; cluster -> complete for addEdge of G,v1,e,v2; end; theorem :: GLIB_006:110 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds G1.order() = G2.order() & G1.size() = G2.size() +` 1; theorem :: GLIB_006:111 for G2 being _finite _Graph, v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds G1.size() = G2.size() + 1; registration let G be _finite _Graph; let v1,e,v2 be object; cluster -> _finite for addEdge of G,v1,e,v2; end; theorem :: GLIB_006:112 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2 holds G1 is loopless; theorem :: GLIB_006:113 for G2 for v being Vertex of G2, e being object for G1 being addEdge of G2,v,e,v st G2 is non loopless or not e in the_Edges_of G2 holds G1 is non loopless; registration let G; let v be Vertex of G; cluster -> non loopless for addEdge of G,v,the_Edges_of G,v; end; theorem :: GLIB_006:114 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st G2 is non-Dmulti & not ex e3 being object st e3 DJoins v1,v2,G2 holds G1 is non-Dmulti; theorem :: GLIB_006:115 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & ex e2 being object st e2 DJoins v1,v2,G2 holds G1 is non non-Dmulti; theorem :: GLIB_006:116 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st G2 is non-multi & not v1,v2 are_adjacent holds G1 is non-multi; theorem :: GLIB_006:117 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v1,v2 are_adjacent holds G1 is non non-multi; theorem :: GLIB_006:118 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st G2 is acyclic & not v2 in G2.reachableFrom v1 holds G1 is acyclic; theorem :: GLIB_006:119 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & v2 in G2.reachableFrom v1 holds G1 is non acyclic; :: this is the theorem that spawned most of the preliminaries, :: although it carries a seemingly obvious meaning. :: it basically states that adding an edge within a component of a graph :: doesn't connect it to other components theorem :: GLIB_006:120 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st G2 is non connected & v2 in G2.reachableFrom v1 holds G1 is non connected; :: this theorem means there is at most one edge missing to completion theorem :: GLIB_006:121 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & (for v3, v4 being Vertex of G2 st not v3,v4 are_adjacent holds (v3 = v4 or (v1 = v3 & v2 = v4) or (v1 = v4 & v2 = v3))) holds G1 is complete; theorem :: GLIB_006:122 for G2 for v1,v2 being Vertex of G2, e being object for G1 being addEdge of G2,v1,e,v2 st G2 is non complete & v1, v2 are_adjacent holds G1 is non complete; definition let G; let v1,e,v2 be object; mode addAdjVertex of G,v1,e,v2 -> Supergraph of G means :: GLIB_006:def 12 the_Vertices_of it = the_Vertices_of G \/ {v2} & the_Edges_of it = the_Edges_of G \/ {e} & the_Source_of it = the_Source_of G +* (e .--> v1) & the_Target_of it = the_Target_of G +* (e .--> v2) if v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G, the_Vertices_of it = the_Vertices_of G \/ {v1} & the_Edges_of it = the_Edges_of G \/ {e} & the_Source_of it = the_Source_of G +* (e .--> v1) & the_Target_of it = the_Target_of G +* (e .--> v2) if not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G otherwise it == G; end; definition let G; let v1 be Vertex of G; let e, v2 be object; redefine mode addAdjVertex of G,v1,e,v2 means :: GLIB_006:def 13 the_Vertices_of it = the_Vertices_of G \/ {v2} & the_Edges_of it = the_Edges_of G \/ {e} & the_Source_of it = the_Source_of G +* (e .--> v1) & the_Target_of it = the_Target_of G +* (e .--> v2) if not v2 in the_Vertices_of G & not e in the_Edges_of G otherwise it == G; end; definition let G; let v1,e be object; let v2 be Vertex of G; redefine mode addAdjVertex of G,v1,e,v2 means :: GLIB_006:def 14 the_Vertices_of it = the_Vertices_of G \/ {v1} & the_Edges_of it = the_Edges_of G \/ {e} & the_Source_of it = the_Source_of G +* (e .--> v1) & the_Target_of it = the_Target_of G +* (e .--> v2) if not v1 in the_Vertices_of G & not e in the_Edges_of G otherwise it == G; end; theorem :: GLIB_006:123 for G for v1,e,v2 being object, G1, G2 being addAdjVertex of G,v1,e,v2 holds G1 == G2; theorem :: GLIB_006:124 for G, G2 for v1,e,v2 being object, G1 being addAdjVertex of G,v1,e,v2 st G1 == G2 holds G2 is addAdjVertex of G,v1,e,v2; theorem :: GLIB_006:125 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds ex G3 being addVertex of G2,v2 st G1 is addEdge of G3,v1,e,v2; theorem :: GLIB_006:126 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds ex G3 being addVertex of G2,v1 st G1 is addEdge of G3,v1,e,v2; theorem :: GLIB_006:127 for G3 being _Graph, v1 being Vertex of G3, e,v2 being object for G2 being addVertex of G3,v2, G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v2 in the_Vertices_of G3 holds G1 is addAdjVertex of G3,v1,e,v2; theorem :: GLIB_006:128 for G3 being _Graph, v1, e being object, v2 being Vertex of G3 for G2 being addVertex of G3,v1, G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G3 & not v1 in the_Vertices_of G3 holds G1 is addAdjVertex of G3,v1,e,v2; theorem :: GLIB_006:129 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds v2 is Vertex of G1; theorem :: GLIB_006:130 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds v1 is Vertex of G1; theorem :: GLIB_006:131 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds e DJoins v1,v2,G1 & e Joins v1,v2,G1; theorem :: GLIB_006:132 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds e DJoins v1,v2,G1 & e Joins v1,v2,G1; theorem :: GLIB_006:133 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 for e1, w being object st (w <> v1 or e1 <> e) holds not e1 Joins w,v2,G1; theorem :: GLIB_006:134 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 for e1, w being object st (w <> v2 or e1 <> e) holds not e1 Joins v1,w,G1; theorem :: GLIB_006:135 for G2 for v1, e, v2 being object for G1 being addAdjVertex of G2,v1,e,v2 holds G1.edgesBetween(the_Vertices_of G2) = the_Edges_of G2; theorem :: GLIB_006:136 for G2 for v1, e, v2 being object for G1 being addAdjVertex of G2,v1,e,v2 holds G2 is inducedSubgraph of G1, the_Vertices_of G2; theorem :: GLIB_006:137 for G2 for v1 being Vertex of G2, e being object, v2 being set for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds G2 is removeVertex of G1, v2; theorem :: GLIB_006:138 for G2 for v1 being set, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds G2 is removeVertex of G1, v1; theorem :: GLIB_006:139 for G being non _trivial _Graph, v1 being Vertex of G, e,v2 being object for G1 being addAdjVertex of G,v1,e,v2 for G2 being removeVertex of G1,v1 for G3 being removeVertex of G,v1 st not e in the_Edges_of G & not v2 in the_Vertices_of G holds G2 is addVertex of G3, v2; theorem :: GLIB_006:140 for G being non _trivial _Graph, v1,e being object, v2 being Vertex of G for G1 being addAdjVertex of G,v1,e,v2 for G2 being removeVertex of G1,v2 for G3 being removeVertex of G,v2 st not e in the_Edges_of G & not v1 in the_Vertices_of G holds G2 is addVertex of G3, v1; :: What has been left out here is the Proof that the vertex to which :: a new vertex with edge is added becomes a cut-vertex in the :: resulting supergraph. A sketch of the Proof is commented below. :: This theorem would be the easy way to show that any vertex in a (non :: trivial) path graph that isn't an endvertex is a cut-vertex. :: :: The difficulty of my Proofs lies in the difficulty of the Proofs of :: the theorems my Proof would need. First there is :: theorem (1) for G2 being non trivial _Graph, v1, e,v2 being object, :: G1 being addAdjVertex of G2,v1,e,v2 :: holds G1.numComponents() = G2.numComponents(); :: which is not hard, just cumbersome. Then :: theorem (2) for G being _Graph, v being Vertex of G, :: G2 being removeVertex of G, v :: st G2.numComponents() in G.numComponents() :: holds v is isolated; :: which is harder than it looks, especially since the converse has :: already been proven in the preliminaries. I found it to need :: theorem (3) for G being _Graph, u,v,w being Vertex of G :: st v is non cut-vertex & u in G.reachableFrom(w) :: holds ex W being Walk st W is_Walk_from w,u & not v in W.vertices(); :: for a contradiction Proof (take v to be non isolated, let w be a :: neighbour of v; v is non cut-vertex by assumption, so use (3) :: to show G2.reachableFrom(w) = G1.reachableFrom(w) \ {v}, :: deduce a bijection between component sets of G1 and G2 leading :: to the contradiction). :: Last theorem is :: theorem (4) for G1 being non trivial _Graph, v being Vertex of G, :: G2 being removeVertex of G1, v :: st v is non isolated non cut-vertex :: holds G1.numComponents() = G2.numComponents(); :: which is just a corrolary of (2) and the definition of cut-vertex. :: Of course (2), (3) and (4) would belong into GLIB_002 to ease theorem :: finding for future articles. :: :: The dedicated reader is welcome to prove these theorems and the main one :: below, or even find a shorter Proof (nevertheless theorems (1)-(3) :: should be added to the MML because they are stating obvious facts). :: ::theorem :: for G2 being non trivial _Graph, v1 being Vertex of G2, e,v2 being object, :: G1 being addAdjVertex of G2,v1,e,v2, w being Vertex of G1 :: st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w = v1 :: & v1 is non isolated :: holds w is cut-vertex; ::proof :: let G2 be non trivial _Graph, v1 be Vertex of G2, e,v2 be object; :: let G1 be addAdjVertex of G2,v1,e,v2, w be Vertex of G1; :: assume A1: not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w=v1 :: & v1 is non isolated; :: for G4 being removeVertex of G1,w holds :: G1.numComponents() in G4.numComponents() :: proof :: let G4 be removeVertex of G1,w; :: set G3 = the removeVertex of G2,v1; :: G4 is removeVertex of G1,v1 by A1; :: G4 is addVertex of G3, v2 :: C(G1) = C(G2) by (1) :: C(G4) = C(G3)+1 :: if v1 is cut-vertex in G2: :: ==> C(G2) in C(G3) :: if C(G4) = C(G1) :: ==> C(G1) = C(G4) = C(G3)+1 :: but C(G1)+1 = C(G2)+1 in C(G3)+1, hence contradiction :: so C(G4) <> C(G1) :: also C(G4) < C(G1) implies w is isolated by (2) :: so C(G4) > C(G1) qed :: if not v1 is cut-vertex in G2: :: v1 is non isolated :: ==> C(G3) = C(G2) by (4) :: ==> C(G4) = C(G1)+1 :: ==> C(G1) in C(G4) qed :: thus thesis; :: end; :: hence thesis by GLIB_002:def 10; ::end; :: also don't forget the symmetric analogon :: (for v1, e being object, v2 being Vertex of G2) theorem :: GLIB_006:141 for G2 for v1 being Vertex of G2, e, v2 being object for G1 being addAdjVertex of G2,v1,e,v2 for w being Vertex of G1 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & w = v2 holds w is endvertex; theorem :: GLIB_006:142 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 for w being Vertex of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & w = v1 holds w is endvertex; theorem :: GLIB_006:143 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds G1 is non _trivial; theorem :: GLIB_006:144 for G2 for v1,e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds G1 is non _trivial; registration let G be _Graph; let v be Vertex of G; cluster -> non _trivial for addAdjVertex of G,v,the_Edges_of G, the_Vertices_of G; cluster -> non _trivial for addAdjVertex of G,the_Vertices_of G,the_Edges_of G, v; end; registration let G be _trivial _Graph; let v be Vertex of G; cluster -> complete for addAdjVertex of G,v,the_Edges_of G,the_Vertices_of G; cluster -> complete for addAdjVertex of G,the_Vertices_of G,the_Edges_of G,v; end; registration let G be loopless _Graph; let v1,e,v2 be object; cluster -> loopless for addAdjVertex of G,v1,e,v2; end; registration let G be non-Dmulti _Graph; let v1,e,v2 be object; cluster -> non-Dmulti for addAdjVertex of G,v1,e,v2; end; registration let G be non-multi _Graph; let v1,e,v2 be object; cluster -> non-multi for addAdjVertex of G,v1,e,v2; end; registration let G be Dsimple _Graph; let v1,e,v2 be object; cluster -> Dsimple for addAdjVertex of G,v1,e,v2; end; registration let G be simple _Graph; let v1,e,v2 be object; cluster -> simple for addAdjVertex of G,v1,e,v2; end; theorem :: GLIB_006:145 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2, W being Walk of G1 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & ((not e in W.edges() & W is non trivial) or not v2 in W.vertices()) holds W is Walk of G2; theorem :: GLIB_006:146 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2, W being Walk of G1 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & ((not e in W.edges() & W is non trivial) or not v1 in W.vertices()) holds W is Walk of G2; theorem :: GLIB_006:147 for G2 for v1, e, v2 being object for G1 being addAdjVertex of G2,v1,e,v2, T being Trail of G1 st not e in the_Edges_of G2 & T.first() in the_Vertices_of G2 & T.last() in the_Vertices_of G2 holds not e in T.edges(); registration let G be connected _Graph; let v1,e,v2 be object; cluster -> connected for addAdjVertex of G,v1,e,v2; end; registration let G be non connected _Graph; let v1,e,v2 be object; cluster -> non connected for addAdjVertex of G,v1,e,v2; end; registration let G be acyclic _Graph; let v1,e,v2 be object; cluster -> acyclic for addAdjVertex of G,v1,e,v2; end; registration let G be Tree-like _Graph; let v1,e,v2 be object; cluster -> Tree-like for addAdjVertex of G,v1,e,v2; end; theorem :: GLIB_006:148 for G2 for v1 being Vertex of G2, e,v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 & G2 is non _trivial holds G1 is non complete; theorem :: GLIB_006:149 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 & G2 is non _trivial holds G1 is non complete; registration let G be non complete _Graph; let v1,e,v2 be object; cluster -> non complete for addAdjVertex of G,v1,e,v2; end; registration let G be non _trivial _Graph; let v be Vertex of G; cluster -> non complete for addAdjVertex of G,v,the_Edges_of G,the_Vertices_of G; cluster -> non complete for addAdjVertex of G,the_Vertices_of G,the_Edges_of G,v; end; theorem :: GLIB_006:150 for G2 for v1 being Vertex of G2, e, v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds G1.order() = G2.order() +` 1 & G1.size() = G2.size() +` 1; theorem :: GLIB_006:151 for G2 for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds G1.order() = G2.order() +` 1 & G1.size() = G2.size() +` 1; theorem :: GLIB_006:152 for G2 being _finite _Graph, v1 being Vertex of G2, e, v2 being object for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v2 in the_Vertices_of G2 holds G1.order() = G2.order() + 1 & G1.size() = G2.size() + 1; theorem :: GLIB_006:153 for G2 being _finite _Graph for v1, e being object, v2 being Vertex of G2 for G1 being addAdjVertex of G2,v1,e,v2 st not e in the_Edges_of G2 & not v1 in the_Vertices_of G2 holds G1.order() = G2.order() + 1 & G1.size() = G2.size() + 1; registration let G be _finite _Graph; let v1,e,v2 be object; cluster -> _finite for addAdjVertex of G,v1,e,v2; end;