:: About Supergraphs, Part {I}
:: by Sebastian Koch
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

:: into ABIAN ?

theorem Th1: :: GLIB_006:1

for n being even Integer
for m being odd Integer st n <= m holds
n + 1 <= m

proof end;

:: into ABIAN ?

theorem Th2: :: GLIB_006:2

for n being even Integer
for m being odd Integer st m <= n holds
m + 1 <= n

proof end;

:: into NAT_D ?

theorem Th3: :: GLIB_006:3

for i, j being Nat st i > (i -' 1) + j holds
j = 0

proof end;

:: BEGIN into FINSEQ_6 or JORDAN4 ?

theorem Th6: :: GLIB_006:4

for f, g being FinSequence
for i being Nat st i <= len f & mid (f,i,((i -' 1) + (len g))) = g holds
(i -' 1) + (len g) <= len f

proof end;

Th7: for p being FinSequence
for n being Nat st n in dom p holds
mid (p,n,n) = <*(p . n)*>
by JORDAN4:15;

Th8: for p being FinSequence
for k1, k2 being Nat st k1 < k2 & k1 in dom p holds
mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))
by FINSEQ_6:126;

theorem Th9: :: GLIB_006:5

for p being FinSequence
for n being Nat st n in dom p & n + 1 <= len p holds
mid (p,n,(n + 1)) = <*(p . n),(p . (n + 1))*>

proof end;

theorem Th10: :: GLIB_006:6

for p being FinSequence
for 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))*>

proof end;

:: 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 Th11: :: GLIB_006:7

for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( not g is_substring_of f,n or len g = 0 or ( 1 <= (n -' 1) + (len g) & (n -' 1) + (len g) <= len f & n <= (n -' 1) + (len g) ) )

proof end;

definition

let D be non empty set ;
let f, g be FinSequence of D;
let 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;

:: deftheorem defines is_odd_substring_of GLIB_006:def 1 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( g is_odd_substring_of f,n iff ( len g > 0 implies ex i being odd Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );

:: deftheorem defines is_even_substring_of GLIB_006:def 2 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( g is_even_substring_of f,n iff ( len g > 0 implies ex i being even Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );

theorem Th12: :: GLIB_006:8

for D being non empty set
for f, g being FinSequence of D
for n being Nat st g is_odd_substring_of f,n holds
g is_substring_of f,n by FINSEQ_8:def 7;

theorem :: GLIB_006:9

for D being non empty set
for f, g being FinSequence of D
for n being Nat st g is_even_substring_of f,n holds
g is_substring_of f,n by FINSEQ_8:def 7;

theorem :: GLIB_006:10

for D being non empty set
for f, g being FinSequence of D
for 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 ) )

proof end;

theorem Th15: :: GLIB_006:11

for D being non empty set
for f being FinSequence of D st 1 <= len f holds
f is_odd_substring_of f, 0

proof end;

theorem Th16: :: GLIB_006:12

for D being non empty set
for f, g being FinSequence of D
for n being even Element of NAT st g is_odd_substring_of f,n holds
g is_odd_substring_of f,n + 1 by Th1;

theorem :: GLIB_006:13

for D being non empty set
for f, g being FinSequence of D
for n being odd Element of NAT st g is_even_substring_of f,n holds
g is_even_substring_of f,n + 1 by Th2;

theorem Th18: :: GLIB_006:14

for D being non empty set
for f, g being FinSequence of D st g is_odd_substring_of f, 0 holds
g is_odd_substring_of f,1

proof end;

:: into GLIB_000 ?

registration

let G be non-Dmulti _Graph;

cluster -> non-Dmulti for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is non-Dmulti

proof end;

end;

:: into GLIB_000 ?

theorem Th19: :: GLIB_006:15

for G being _Graph holds G is inducedSubgraph of G,(the_Vertices_of G)

proof end;

:: into GLIB_000 ?

theorem Th20: :: GLIB_006:16

for G1, G3 being _Graph
for V, E being set
for G2 being inducedSubgraph of G1,V,E st G2 == G3 holds
G3 is inducedSubgraph of G1,V,E

proof end;

:: into GLIB_000 ?

theorem Th21: :: GLIB_006:17

for G being _Graph
for X being set
for e, y being object st e SJoins X,{y},G holds
ex x being object st
( x in X & e Joins x,y,G )

proof end;

:: into GLIB_000 ?

theorem :: GLIB_006:18

for G being _Graph
for X being set st X /\ (the_Vertices_of G) = {} holds
( G .edgesInto X = {} & G .edgesOutOf X = {} & G .edgesInOut X = {} & G .edgesBetween X = {} )

proof end;

:: into GLIB_000 ?

theorem :: GLIB_006:19

for G being _Graph
for X1, X2 being set
for y being object st X1 misses X2 holds
G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y})

proof end;

:: into GLIB_000 ?

theorem :: GLIB_006:20

for G being _Graph
for X1, X2 being set
for y being object holds G .edgesBetween ((X1 \/ X2),{y}) = (G .edgesBetween (X1,{y})) \/ (G .edgesBetween (X2,{y}))

proof end;

:: 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 )

proof end;

:: definitely into GLIB_001

registration

let G be _Graph;

cluster V5() closed Trail-like -> Circuit-like for Walk of G;

coherence
for b₁ being Walk of G st b₁ is closed & b₁ is Trail-like & b₁ is V5() holds
b₁ is Circuit-like by GLIB_001:def 30;

cluster V5() closed Path-like -> Cycle-like for Walk of G;

coherence
for b₁ being Walk of G st b₁ is closed & b₁ is Path-like & b₁ is V5() holds
b₁ is Cycle-like by GLIB_001:def 31;

end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?

theorem Th26: :: GLIB_006:22

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Trail-like holds
W2 is Trail-like

proof end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?

theorem Th27: :: GLIB_006:23

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Path-like holds
W2 is Path-like

proof end;

:: 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
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is Cycle-like holds
W2 is Cycle-like

proof end;

:: generalizes part of GLIB_001:175 and GLIB_001:176
:: into GLIB_001 ?

theorem :: GLIB_006:25

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is vertex-distinct holds
W2 is vertex-distinct

proof end;

:: 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
for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
G .walkOf v is_substring_of W, 0

proof end;

theorem Th31: :: GLIB_006:27

for G being _Graph
for W being Walk of G
for 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

proof end;

theorem :: GLIB_006:28

for G being _Graph
for W being Walk of G
for u, e, v being object st e Joins u,v,G & e in W .edges() & not G .walkOf (u,e,v) is_odd_substring_of W, 0 holds
G .walkOf (v,e,u) is_odd_substring_of W, 0

proof end;

theorem :: GLIB_006:29

for G being _Graph
for W being Walk of G
for 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() )

proof end;

definition

let G be _Graph;
let W1, W2 be Walk of G;

func W1 .findFirstVertex W2 -> odd Element of NAT means :Def3: :: 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;

existence
( ( W2 is_odd_substring_of W1, 0 implies ex b₁ being odd Element of NAT st
( b₁ <= len W1 & ex k being even Nat st
( b₁ = 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 ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ex b₁ being odd Element of NAT st b₁ = len W1 ) )

proof end;

uniqueness
for b₁, b₂ being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 & b₁ <= len W1 & ex k being even Nat st
( b₁ = 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 ) ) & b₂ <= len W1 & ex k being even Nat st
( b₂ = 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 ) ) implies b₁ = b₂ ) & ( not W2 is_odd_substring_of W1, 0 & b₁ = len W1 & b₂ = len W1 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being odd Element of NAT holds verum ;

func W1 .findLastVertex W2 -> odd Element of NAT means :Def4: :: 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;

existence
( ( W2 is_odd_substring_of W1, 0 implies ex b₁ being odd Element of NAT st
( b₁ <= len W1 & ex k being even Nat st
( b₁ = 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 ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ex b₁ being odd Element of NAT st b₁ = len W1 ) )

proof end;

uniqueness
for b₁, b₂ being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 & b₁ <= len W1 & ex k being even Nat st
( b₁ = 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 ) ) & b₂ <= len W1 & ex k being even Nat st
( b₂ = 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 ) ) implies b₁ = b₂ ) & ( not W2 is_odd_substring_of W1, 0 & b₁ = len W1 & b₂ = len W1 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being odd Element of NAT holds verum ;

end;

:: deftheorem Def3 defines .findFirstVertex GLIB_006:def 3 :
for G being _Graph
for W1, W2 being Walk of G
for b₄ being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 implies ( b₄ = W1 .findFirstVertex W2 iff ( b₄ <= len W1 & ex k being even Nat st
( b₄ = 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 ) ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ( b₄ = W1 .findFirstVertex W2 iff b₄ = len W1 ) ) );

:: deftheorem Def4 defines .findLastVertex GLIB_006:def 4 :
for G being _Graph
for W1, W2 being Walk of G
for b₄ being odd Element of NAT holds
( ( W2 is_odd_substring_of W1, 0 implies ( b₄ = W1 .findLastVertex W2 iff ( b₄ <= len W1 & ex k being even Nat st
( b₄ = 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 ) ) ) ) ) & ( not W2 is_odd_substring_of W1, 0 implies ( b₄ = W1 .findLastVertex W2 iff b₄ = len W1 ) ) );

theorem Th34: :: GLIB_006:30

for G being _Graph
for 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() )

proof end;

theorem Th35: :: GLIB_006:31

for G being _Graph
for 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 ) by Def3, Def4, ABIAN:12;

theorem Th36: :: GLIB_006:32

for G being _Graph
for W being Walk of G holds
( 1 = W .findFirstVertex W & W .findLastVertex W = len W )

proof end;

theorem :: GLIB_006:33

for G being _Graph
for W1, W2 being Walk of G st W2 is_odd_substring_of W1, 0 holds
W1 .findFirstVertex W2 <= W1 .findLastVertex W2

proof end;

definition

let G be _Graph;
let W1, W2, W3 be Walk of G;

func W1 .replaceWith (W2,W3) -> Walk of G equals :Def5: :: 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;

correctness
coherence
( ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() implies ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1))) is Walk of G ) & ( ( not W2 is_odd_substring_of W1, 0 or not W2 .first() = W3 .first() or not W2 .last() = W3 .last() ) implies W1 is Walk of G ) );
consistency
for b₁ being Walk of G holds verum;
;

end;

:: deftheorem Def5 defines .replaceWith GLIB_006:def 5 :
for G being _Graph
for W1, W2, W3 being Walk of G holds
( ( W2 is_odd_substring_of W1, 0 & W2 .first() = W3 .first() & W2 .last() = W3 .last() implies W1 .replaceWith (W2,W3) = ((W1 .cut (1,(W1 .findFirstVertex W2))) .append W3) .append (W1 .cut ((W1 .findLastVertex W2),(len W1))) ) & ( ( not W2 is_odd_substring_of W1, 0 or not W2 .first() = W3 .first() or not W2 .last() = W3 .last() ) implies W1 .replaceWith (W2,W3) = W1 ) );

definition

let G be _Graph;
let W1, W3 be Walk of G;
let e be object ;

func W1 .replaceEdgeWith (e,W3) -> Walk of G equals :Def6: :: 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;

correctness
coherence
( ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 implies W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) is Walk of G ) & ( ( not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) implies W1 is Walk of G ) );
consistency
for b₁ being Walk of G holds verum;
;

end;

:: deftheorem Def6 defines .replaceEdgeWith GLIB_006:def 6 :
for G being _Graph
for W1, W3 being Walk of G
for e being object holds
( ( e Joins W3 .first() ,W3 .last() ,G & G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 implies W1 .replaceEdgeWith (e,W3) = W1 .replaceWith ((G .walkOf ((W3 .first()),e,(W3 .last()))),W3) ) & ( ( not e Joins W3 .first() ,W3 .last() ,G or not G .walkOf ((W3 .first()),e,(W3 .last())) is_odd_substring_of W1, 0 ) implies W1 .replaceEdgeWith (e,W3) = W1 ) );

definition

let G be _Graph;
let W1, W2 be Walk of G;
let e be object ;

func W1 .replaceWithEdge (W2,e) -> Walk of G equals :Def7: :: 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;

correctness
coherence
( ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G implies W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last())))) is Walk of G ) & ( ( not W2 is_odd_substring_of W1, 0 or not e Joins W2 .first() ,W2 .last() ,G ) implies W1 is Walk of G ) );
consistency
for b₁ being Walk of G holds verum;
;

end;

:: deftheorem Def7 defines .replaceWithEdge GLIB_006:def 7 :
for G being _Graph
for W1, W2 being Walk of G
for e being object holds
( ( W2 is_odd_substring_of W1, 0 & e Joins W2 .first() ,W2 .last() ,G implies W1 .replaceWithEdge (W2,e) = W1 .replaceWith (W2,(G .walkOf ((W2 .first()),e,(W2 .last())))) ) & ( ( not W2 is_odd_substring_of W1, 0 or not e Joins W2 .first() ,W2 .last() ,G ) implies W1 .replaceWithEdge (W2,e) = W1 ) );

theorem Th38: :: GLIB_006:34

for G being _Graph
for 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() )

proof end;

theorem Th39: :: GLIB_006:35

for G being _Graph
for W1, W2, W3 being Walk of G holds
( W1 .first() = (W1 .replaceWith (W2,W3)) .first() & W1 .last() = (W1 .replaceWith (W2,W3)) .last() )

proof end;

theorem :: GLIB_006:36

for G being _Graph
for 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())

proof end;

theorem Th41: :: GLIB_006:37

for G being _Graph
for 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())

proof end;

theorem Th42: :: GLIB_006:38

for G being _Graph
for W1, W3 being Walk of G
for 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() ) )

proof end;

:: The Proof got surprisingly long. Maybe there's a shorter way?

theorem Th43: :: GLIB_006:39

for G being _Graph
for W1, W3 being Walk of G
for 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()

proof end;

:: 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 Th44: :: GLIB_006:40

for G being _Graph
for T1 being Trail of G
for W3 being Walk of G
for 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()

proof end;

theorem :: GLIB_006:41

for G being _Graph
for W1, W2 being Walk of G st W1 .first() = W2 .first() & W1 .last() = W2 .last() holds
W1 .replaceWith (W1,W2) = W2

proof end;

:: 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 Th46: :: GLIB_006:42

for G being _Graph
for W1, W3 being Walk of G
for 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)

proof end;

:: same as theorem above

theorem Th47: :: GLIB_006:43

for G being _Graph
for W1, W2 being Walk of G
for 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)

proof end;

theorem :: GLIB_006:44

for G being _Graph
for W1, W3 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceEdgeWith (e,W3)) .first() & W1 .last() = (W1 .replaceEdgeWith (e,W3)) .last() )

proof end;

theorem :: GLIB_006:45

for G being _Graph
for W1, W2 being Walk of G
for e being object holds
( W1 .first() = (W1 .replaceWithEdge (W2,e)) .first() & W1 .last() = (W1 .replaceWithEdge (W2,e)) .last() )

proof end;

theorem Th50: :: GLIB_006:46

for G being _Graph
for W1, W2, W3 being Walk of G
for u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceWith (W2,W3) is_Walk_from u,v )

proof end;

theorem Th51: :: GLIB_006:47

for G being _Graph
for W1, W3 being Walk of G
for e, u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceEdgeWith (e,W3) is_Walk_from u,v )

proof end;

theorem :: GLIB_006:48

for G being _Graph
for W1, W2 being Walk of G
for e, u, v being object holds
( W1 is_Walk_from u,v iff W1 .replaceWithEdge (W2,e) is_Walk_from u,v )

proof end;

:: END into GLIB_001 ?
:: into GLIB_002 ?

theorem Th53: :: GLIB_006:49

for G being _Graph
for v1, v2 being Vertex of G st v1 is isolated & v1 <> v2 holds
not v2 in G .reachableFrom v1

proof end;

:: into GLIB_002 ?

theorem Th54: :: GLIB_006:50

for G being _Graph
for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
v2 in G .reachableFrom v1

proof end;

:: into GLIB_002 ?

theorem Th55: :: GLIB_006:51

for G being _Graph
for v being Vertex of G st v is isolated holds
{v} = G .reachableFrom v

proof end;

:: into GLIB_002 ?

theorem :: GLIB_006:52

for G being _Graph
for v being Vertex of G
for C being inducedSubgraph of G,{v} st v is isolated holds
C is Component of G

proof end;

:: into GLIB_002 ?

theorem Th57: :: GLIB_006:53

for G1 being non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is isolated holds
( G1 .componentSet() = (G2 .componentSet()) \/ {{v}} & G1 .numComponents() = (G2 .numComponents()) +` 1 )

proof end;

:: into GLIB_002 ?

registration

let G be _Graph;

cluster isolated -> non cut-vertex for Element of the_Vertices_of G;

coherence
for b₁ being Vertex of G st b₁ is isolated holds
not b₁ is cut-vertex

proof end;

end;

:: into GLIB_002 ?

theorem Th58: :: GLIB_006:54

for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is Cycle-like iff W2 is Cycle-like )

proof end;

:: into GLIB_002 ?

theorem :: GLIB_006:55

for G1 being connected _Graph
for G2 being Component of G1 holds G1 == G2

proof end;

:: into CHORD ?

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] complete -> connected for set ;

coherence
for b₁ being _Graph st b₁ is complete holds
b₁ is connected

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] non _finite non loopless non non-multi non non-Dmulti non simple non Dsimple non acyclic for set ;

existence
ex b₁ being _Graph st
( not b₁ is non-Dmulti & not b₁ is non-multi & not b₁ is loopless & not b₁ is Dsimple & not b₁ is simple & not b₁ is acyclic & not b₁ is _finite )

proof end;

end;

definition

let G be _Graph;

func Endvertices G -> Subset of (the_Vertices_of G) means :Def8: :: 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 ) );

existence
ex b₁ being Subset of (the_Vertices_of G) st
for v being object holds
( v in b₁ iff ex w being Vertex of G st
( v = w & w is endvertex ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (the_Vertices_of G) st ( for v being object holds
( v in b₁ iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ) & ( for v being object holds
( v in b₂ iff ex w being Vertex of G st
( v = w & w is endvertex ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Endvertices GLIB_006:def 8 :
for G being _Graph
for b₂ being Subset of (the_Vertices_of G) holds
( b₂ = Endvertices G iff for v being object holds
( v in b₂ iff ex w being Vertex of G st
( v = w & w is endvertex ) ) );

theorem :: GLIB_006:56

for G being _Graph
for v being Vertex of G holds
( v in Endvertices G iff v is endvertex )

proof end;

:: analogue to GLIB_000:def 32

definition

let G be _Graph;

mode Supergraph of G -> _Graph means :Def9: :: 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 ) ) );

existence
ex b₁ being _Graph st
( the_Vertices_of G c= the_Vertices_of b₁ & the_Edges_of G c= the_Edges_of b₁ & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of b₁) . e & (the_Target_of G) . e = (the_Target_of b₁) . e ) ) )

proof end;

end;

:: deftheorem Def9 defines Supergraph GLIB_006:def 9 :
for G, b₂ being _Graph holds
( b₂ is Supergraph of G iff ( the_Vertices_of G c= the_Vertices_of b₂ & the_Edges_of G c= the_Edges_of b₂ & ( for e being set st e in the_Edges_of G holds
( (the_Source_of G) . e = (the_Source_of b₂) . e & (the_Target_of G) . e = (the_Target_of b₂) . e ) ) ) );

:: 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 Th61: :: GLIB_006:57

for G1, G2 being _Graph holds
( G2 is Subgraph of G1 iff G1 is Supergraph of G2 )

proof end;

theorem Th62: :: GLIB_006:58

for G1, G2 being _Graph holds
( ( G2 is Subgraph of G1 & G2 is Supergraph of G1 ) iff G1 == G2 )

proof end;

theorem Th63: :: GLIB_006:59

for G1, G2 being _Graph holds
( ( G1 is Supergraph of G2 & G2 is Supergraph of G1 ) iff G1 == G2 )

proof end;

theorem Th64: :: GLIB_006:60

for G1, G2 being _Graph holds
( G1 is Supergraph of G2 iff G2 c= G1 )

proof end;

theorem Th65: :: GLIB_006:61

for G being _Graph holds G is Supergraph of G by Th64;

theorem Th66: :: GLIB_006:62

for G3 being _Graph
for G2 being Supergraph of G3
for G1 being Supergraph of G2 holds G1 is Supergraph of G3

proof end;

:: the following 4 Supergraph theorems have no Subgraph analogon in the MML yet

theorem Th67: :: 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

proof end;

theorem Th68: :: GLIB_006:64

for G2 being _Graph
for G1 being Supergraph of G2 holds
( the_Source_of G2 c= the_Source_of G1 & the_Target_of G2 c= the_Target_of G1 )

proof end;

theorem Th69: :: GLIB_006:65

for G2 being _Graph
for G1 being Supergraph of G2 st the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 holds
G1 == G2

proof end;

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

proof end;

theorem Th71: :: GLIB_006:67

for G2 being _Graph
for G1 being Supergraph of G2
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 ) )

proof end;

theorem Th72: :: GLIB_006:68

for G2 being _Graph
for G1 being Supergraph of G2
for v being Vertex of G2 holds v is Vertex of G1 by Th71;

theorem :: GLIB_006:69

for G2 being _Graph
for G1 being Supergraph of G2 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) )

proof end;

theorem Th74: :: GLIB_006:70

for G2 being _Graph
for G1 being Supergraph of G2
for x, y being set
for 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 ) )

proof end;

theorem Th75: :: GLIB_006:71

for G2 being _Graph
for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e DJoins v1,v2,G1 or e DJoins v1,v2,G2 or not e in the_Edges_of G2 )

proof end;

theorem Th76: :: GLIB_006:72

for G2 being _Graph
for G1 being Supergraph of G2
for e, v1, v2 being object holds
( not e Joins v1,v2,G1 or e Joins v1,v2,G2 or not e in the_Edges_of G2 )

proof end;

registration

let G be _finite _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite for Supergraph of G;

existence
ex b₁ being Supergraph of G st b₁ is _finite

proof end;

end;

:: no equivalent in GLIB_000

theorem :: GLIB_006:73

for G2 being _Graph
for G1 being Supergraph of G2 holds
( G2 .order() c= G1 .order() & G2 .size() c= G1 .size() )

proof end;

theorem :: GLIB_006:74

for G2 being _finite _Graph
for G1 being _finite Supergraph of G2 holds
( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )

proof end;

theorem Th79: :: GLIB_006:75

for G2 being _Graph
for G1 being Supergraph of G2
for W being Walk of G2 holds W is Walk of G1

proof end;

theorem Th80: :: GLIB_006:76

for G2 being _Graph
for G1 being Supergraph of G2
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is V5() implies W2 is V5() ) & ( W2 is V5() implies W1 is V5() ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) & ( W1 is Cycle-like implies W2 is Cycle-like ) & ( W2 is Cycle-like implies W1 is Cycle-like ) )

proof end;

registration

let G be non _trivial _Graph;

cluster -> non _trivial for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is _trivial

proof end;

end;

registration

let G be non non-Dmulti _Graph;

cluster -> non non-Dmulti for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is non-Dmulti

proof end;

end;

registration

let G be non non-multi _Graph;

cluster -> non non-multi for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is non-multi

proof end;

end;

registration

let G be non loopless _Graph;

cluster -> non loopless for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is loopless

proof end;

end;

registration

let G be non Dsimple _Graph;

cluster -> non Dsimple for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is Dsimple

proof end;

end;

registration

let G be non simple _Graph;

cluster -> non simple for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is simple

proof end;

end;

registration

let G be non acyclic _Graph;

cluster -> non acyclic for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is acyclic

proof end;

end;

registration

let G be non _finite _Graph;

cluster -> non _finite for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ is _finite

proof end;

end;

definition

let G be _Graph;
let V be set ;

mode addVertices of G,V -> Supergraph of G means :Def10: :: 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 );

existence
ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ V & the_Edges_of b₁ = the_Edges_of G & the_Source_of b₁ = the_Source_of G & the_Target_of b₁ = the_Target_of G )

proof end;

end;

:: deftheorem Def10 defines addVertices GLIB_006:def 10 :
for G being _Graph
for V being set
for b₃ being Supergraph of G holds
( b₃ is addVertices of G,V iff ( the_Vertices_of b₃ = (the_Vertices_of G) \/ V & the_Edges_of b₃ = the_Edges_of G & the_Source_of b₃ = the_Source_of G & the_Target_of b₃ = the_Target_of G ) );

theorem :: GLIB_006:77

for G being _Graph
for V being set
for G1, G2 being addVertices of G,V holds G1 == G2

proof end;

theorem Th82: :: GLIB_006:78

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 == G2 iff V c= the_Vertices_of G2 )

proof end;

theorem :: GLIB_006:79

for G1, G2 being _Graph
for V being set st G1 == G2 & V c= the_Vertices_of G2 holds
G1 is addVertices of G2,V

proof end;

theorem :: GLIB_006:80

for G, G2 being _Graph
for V being set
for G1 being addVertices of G,V st G1 == G2 holds
G2 is addVertices of G,V

proof end;

theorem Th85: :: GLIB_006:81

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1

proof end;

theorem :: GLIB_006:82

for G3 being _Graph
for V1, V2 being set
for G2 being addVertices of G3,V2
for G1 being addVertices of G2,V1 holds G1 is addVertices of G3,V1 \/ V2

proof end;

theorem :: GLIB_006:83

for G3 being _Graph
for V1, V2 being set
for G1 being addVertices of G3,V1 \/ V2 ex G2 being addVertices of G3,V2 st G1 is addVertices of G2,V1

proof end;

theorem Th88: :: GLIB_006:84

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds G2 is inducedSubgraph of G1,(the_Vertices_of G2)

proof end;

theorem Th89: :: GLIB_006:85

for G2 being _Graph
for V being set
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 )

proof end;

theorem Th90: :: GLIB_006:86

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for v being object st v in V holds
v is Vertex of G1

proof end;

theorem Th91: :: GLIB_006:87

for G2 being _Graph
for V being set
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 )

proof end;

theorem Th92: :: GLIB_006:88

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for v being Vertex of G1 st v in V \ (the_Vertices_of G2) holds
( v is isolated & not v is cut-vertex )

proof end;

theorem Th93: :: GLIB_006:89

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
( not G1 is _trivial & not G1 is connected & not G1 is Tree-like & not G1 is complete )

proof end;

registration

let G be non-Dmulti _Graph;
let V be set ;

cluster -> non-Dmulti for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is non-Dmulti

proof end;

end;

registration

let G be non-multi _Graph;
let V be set ;

cluster -> non-multi for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is non-multi

proof end;

end;

registration

let G be loopless _Graph;
let V be set ;

cluster -> loopless for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is loopless

proof end;

end;

registration

let G be Dsimple _Graph;
let V be set ;

cluster -> Dsimple for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is Dsimple ;

end;

registration

let G be Dsimple _Graph;
let V be set ;

cluster -> Dsimple for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is Dsimple ;

end;

theorem Th94: :: GLIB_006:90

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for W being Walk of G1 holds
( W .vertices() misses V \ (the_Vertices_of G2) or not W is V5() )

proof end;

theorem Th95: :: GLIB_006:91

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for W being Walk of G1 st W .vertices() misses V \ (the_Vertices_of G2) holds
W is Walk of G2

proof end;

registration

let G be acyclic _Graph;
let V be set ;

cluster -> acyclic for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is acyclic

proof end;

end;

theorem Th96: :: GLIB_006:92

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G2 is chordal iff G1 is chordal )

proof end;

:: "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;

coherence
for b₁ being addVertices of G,V holds b₁ is chordal by Th96;

end;

definition

let G be _Graph;
let v be object ;
mode addVertex of G,v is addVertices of G,{v};

end;

theorem :: GLIB_006:93

for G2 being _Graph
for v being object
for G1 being addVertex of G2,v holds
( G1 == G2 iff v in the_Vertices_of G2 ) by Th82, ZFMISC_1:31;

theorem Th98: :: GLIB_006:94

for G2 being _Graph
for v being object
for G1 being addVertex of G2,v holds v is Vertex of G1

proof end;

Lm1: for X being set holds {X} \ X <> {}

proof end;

registration

let G be _Graph;

cluster -> non _trivial non connected non complete for addVertices of G,{(the_Vertices_of G)};

coherence
for b₁ being addVertex of G,(the_Vertices_of G) holds
( not b₁ is _trivial & not b₁ is connected & not b₁ is complete )

proof end;

end;

:: the prime example of how to use the new modes to show existences
:: of certain graphs

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] non _trivial non connected non complete for set ;

existence
ex b₁ being _Graph st
( not b₁ is _trivial & not b₁ is connected & not b₁ is complete )

proof end;

end;

registration

let G be non connected _Graph;
let V be set ;

cluster -> non connected for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds not b₁ is connected

proof end;

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 Th99: :: GLIB_006:95

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 .size() = G2 .size() & G1 .order() = (G2 .order()) +` (card (V \ (the_Vertices_of G2))) )

proof end;

theorem Th100: :: GLIB_006:96

for G2 being _finite _Graph
for V being finite set
for G1 being addVertices of G2,V holds G1 .order() = (G2 .order()) + (card (V \ (the_Vertices_of G2)))

proof end;

theorem :: GLIB_006:97

for G2 being _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) +` 1

proof end;

theorem :: GLIB_006:98

for G2 being _finite _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1

proof end;

registration

let G be _finite _Graph;
let V be finite set ;

cluster -> _finite for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ is _finite

proof end;

end;

registration

let G be _finite _Graph;
let v be object ;

cluster -> _finite for addVertices of G,{v};

coherence
for b₁ being addVertex of G,v holds b₁ is _finite ;

end;

registration

let G be _Graph;
let V be non finite set ;

cluster -> non _finite for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds not b₁ is _finite

proof end;

end;

:: we explicitly add an edge only if it is not used already
:: to ensure getting a Supergraph

definition

let G be _Graph;
let v1, e, v2 be object ;

mode addEdge of G,v1,e,v2 -> Supergraph of G means :Def11: :: 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;

existence
( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = the_Vertices_of G & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) & ( ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b₁ being Supergraph of G st b₁ == G ) )

proof end;

consistency
for b₁ being Supergraph of G holds verum ;

end;

:: deftheorem Def11 defines addEdge GLIB_006:def 11 :
for G being _Graph
for v1, e, v2 being object
for b₅ being Supergraph of G holds
( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addEdge of G,v1,e,v2 iff ( the_Vertices_of b₅ = the_Vertices_of G & the_Edges_of b₅ = (the_Edges_of G) \/ {e} & the_Source_of b₅ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₅ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( not v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₅ is addEdge of G,v1,e,v2 iff b₅ == G ) ) );

theorem :: GLIB_006:99

for G being _Graph
for v1, e, v2 being object
for G1, G2 being addEdge of G,v1,e,v2 holds G1 == G2

proof end;

theorem :: GLIB_006:100

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds
( G1 == G2 iff e in the_Edges_of G2 )

proof end;

theorem :: GLIB_006:101

for G, G2 being _Graph
for v1, e, v2 being object
for G1 being addEdge of G,v1,e,v2 st G1 == G2 holds
G2 is addEdge of G,v1,e,v2

proof end;

theorem Th106: :: GLIB_006:102

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds the_Vertices_of G1 = the_Vertices_of G2

proof end;

theorem :: GLIB_006:103

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 holds G1 .edgesBetween (the_Vertices_of G2) = the_Edges_of G1

proof end;

theorem Th108: :: GLIB_006:104

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for v being Vertex of G1 holds v is Vertex of G2

proof end;

theorem Th109: :: GLIB_006:105

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
e DJoins v1,v2,G1

proof end;

theorem Th110: :: GLIB_006:106

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 holds
e1 = e

proof end;

theorem :: GLIB_006:107

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
for e1, w1, w2 being object st e1 Joins w1,w2,G1 & not e1 in the_Edges_of G2 & not ( w1 = v1 & w2 = v2 ) holds
( w1 = v2 & w2 = v1 )

proof end;

theorem Th112: :: GLIB_006:108

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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

proof end;

theorem Th113: :: GLIB_006:109

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for W being Walk of G1 st ( e in W .edges() implies e in the_Edges_of G2 ) holds
W is Walk of G2

proof end;

registration

let G be _trivial _Graph;
let v1, e, v2 be object ;

cluster -> _trivial for addEdge of G,v1,e,v2;

coherence
for b₁ being addEdge of G,v1,e,v2 holds b₁ is _trivial

proof end;

end;

registration

let G be connected _Graph;
let v1, e, v2 be object ;

cluster -> connected for addEdge of G,v1,e,v2;

coherence
for b₁ being addEdge of G,v1,e,v2 holds b₁ is connected

proof end;

end;

registration

let G be complete _Graph;
let v1, e, v2 be object ;

cluster -> complete for addEdge of G,v1,e,v2;

coherence
for b₁ being addEdge of G,v1,e,v2 holds b₁ is complete

proof end;

end;

theorem :: GLIB_006:110

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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 )

proof end;

theorem :: GLIB_006:111

for G2 being _finite _Graph
for v1, v2 being Vertex of G2
for 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

proof end;

registration

let G be _finite _Graph;
let v1, e, v2 be object ;

cluster -> _finite for addEdge of G,v1,e,v2;

coherence
for b₁ being addEdge of G,v1,e,v2 holds b₁ is _finite

proof end;

end;

theorem Th116: :: GLIB_006:112

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is loopless & v1 <> v2 holds
G1 is loopless

proof end;

theorem Th117: :: GLIB_006:113

for G2 being _Graph
for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v st ( not G2 is loopless or not e in the_Edges_of G2 ) holds
not G1 is loopless

proof end;

registration

let G be _Graph;
let v be Vertex of G;

cluster -> non loopless for addEdge of G,v, the_Edges_of G,v;

coherence
for b₁ being addEdge of G,v, the_Edges_of G,v holds not b₁ is loopless

proof end;

end;

theorem Th118: :: GLIB_006:114

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st G2 is non-Dmulti & ( for e3 being object holds not e3 DJoins v1,v2,G2 ) holds
G1 is non-Dmulti

proof end;

theorem :: GLIB_006:115

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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
not G1 is non-Dmulti

proof end;

theorem Th120: :: GLIB_006:116

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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

proof end;

theorem :: GLIB_006:117

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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
not G1 is non-multi

proof end;

theorem Th122: :: GLIB_006:118

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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

proof end;

theorem :: GLIB_006:119

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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
not G1 is acyclic

proof end;

:: 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 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not G2 is connected & v2 in G2 .reachableFrom v1 holds
not G1 is connected

proof end;

:: this theorem means there is at most one edge missing to completion

theorem :: GLIB_006:121

for G2 being _Graph
for v1, v2 being Vertex of G2
for 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 holds
( v3,v4 are_adjacent or v3 = v4 or ( v1 = v3 & v2 = v4 ) or ( v1 = v4 & v2 = v3 ) ) ) holds
G1 is complete

proof end;

theorem :: GLIB_006:122

for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not G2 is complete & v1,v2 are_adjacent holds
not G1 is complete

proof end;

definition

let G be _Graph;
let v1, e, v2 be object ;

mode addAdjVertex of G,v1,e,v2 -> Supergraph of G means :Def12: :: 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;

existence
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v2} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) & ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v1} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) & ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ex b₁ being Supergraph of G st b₁ == G ) )

proof end;

consistency
for b₁ being Supergraph of G st v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G & not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G holds
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v2} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) iff ( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v1} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) ;

end;

:: deftheorem Def12 defines addAdjVertex GLIB_006:def 12 :
for G being _Graph
for v1, e, v2 being object
for b₅ being Supergraph of G holds
( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₅ = (the_Vertices_of G) \/ {v2} & the_Edges_of b₅ = (the_Edges_of G) \/ {e} & the_Source_of b₅ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₅ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( not v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₅ = (the_Vertices_of G) \/ {v1} & the_Edges_of b₅ = (the_Edges_of G) \/ {e} & the_Source_of b₅ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₅ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( not v1 in the_Vertices_of G or v2 in the_Vertices_of G or e in the_Edges_of G ) & ( v1 in the_Vertices_of G or not v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₅ is addAdjVertex of G,v1,e,v2 iff b₅ == G ) ) );

definition

let G be _Graph;
let v1 be Vertex of G;
let e, v2 be object ;

redefine mode addAdjVertex of G,v1,e,v2 means :Def13: :: 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;

compatibility
for b₁ being Supergraph of G holds
( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₁ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v2} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₁ is addAdjVertex of G,v1,e,v2 iff b₁ == G ) ) ) by Def12;
consistency
for b₁ being Supergraph of G holds verum ;

end;

:: deftheorem Def13 defines addAdjVertex GLIB_006:def 13 :
for G being _Graph
for v1 being Vertex of G
for e, v2 being object
for b₅ being Supergraph of G holds
( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₅ = (the_Vertices_of G) \/ {v2} & the_Edges_of b₅ = (the_Edges_of G) \/ {e} & the_Source_of b₅ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₅ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₅ is addAdjVertex of G,v1,e,v2 iff b₅ == G ) ) );

definition

let G be _Graph;
let v1, e be object ;
let v2 be Vertex of G;

redefine mode addAdjVertex of G,v1,e,v2 means :Def14: :: 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;

compatibility
for b₁ being Supergraph of G holds
( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b₁ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v1} & the_Edges_of b₁ = (the_Edges_of G) \/ {e} & the_Source_of b₁ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₁ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v1 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₁ is addAdjVertex of G,v1,e,v2 iff b₁ == G ) ) ) by Def12;
consistency
for b₁ being Supergraph of G holds verum ;

end;

:: deftheorem Def14 defines addAdjVertex GLIB_006:def 14 :
for G being _Graph
for v1, e being object
for v2 being Vertex of G
for b₅ being Supergraph of G holds
( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b₅ is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b₅ = (the_Vertices_of G) \/ {v1} & the_Edges_of b₅ = (the_Edges_of G) \/ {e} & the_Source_of b₅ = (the_Source_of G) +* (e .--> v1) & the_Target_of b₅ = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v1 in the_Vertices_of G or e in the_Edges_of G ) implies ( b₅ is addAdjVertex of G,v1,e,v2 iff b₅ == G ) ) );

theorem :: GLIB_006:123

for G being _Graph
for v1, e, v2 being object
for G1, G2 being addAdjVertex of G,v1,e,v2 holds G1 == G2

proof end;

theorem :: GLIB_006:124

for G, G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G,v1,e,v2 st G1 == G2 holds
G2 is addAdjVertex of G,v1,e,v2

proof end;

theorem Th129: :: GLIB_006:125

for G2 being _Graph
for v1 being Vertex of G2
for 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

proof end;

theorem Th130: :: GLIB_006:126

for G2 being _Graph
for v1, e being object
for 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

proof end;

theorem :: GLIB_006:127

for G3 being _Graph
for v1 being Vertex of G3
for e, v2 being object
for G2 being addVertex of G3,v2
for 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

proof end;

theorem :: GLIB_006:128

for G3 being _Graph
for v1, e being object
for v2 being Vertex of G3
for G2 being addVertex of G3,v1
for 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

proof end;

theorem Th133: :: GLIB_006:129

for G2 being _Graph
for v1 being Vertex of G2
for 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

proof end;

theorem Th134: :: GLIB_006:130

for G2 being _Graph
for v1, e being object
for 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

proof end;

theorem Th135: :: GLIB_006:131

for G2 being _Graph
for v1 being Vertex of G2
for 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 )

proof end;

theorem Th136: :: GLIB_006:132

for G2 being _Graph
for v1, e being object
for 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 )

proof end;

theorem Th137: :: GLIB_006:133

for G2 being _Graph
for v1 being Vertex of G2
for 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
for e1, w being object st ( w <> v1 or e1 <> e ) holds
not e1 Joins w,v2,G1

proof end;

theorem Th138: :: GLIB_006:134

for G2 being _Graph
for v1, e being object
for 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
for e1, w being object st ( w <> v2 or e1 <> e ) holds
not e1 Joins v1,w,G1

proof end;

theorem Th139: :: GLIB_006:135

for G2 being _Graph
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

proof end;

theorem Th140: :: GLIB_006:136

for G2 being _Graph
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)

proof end;

theorem Th141: :: GLIB_006:137

for G2 being _Graph
for v1 being Vertex of G2
for e being object
for 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

proof end;

theorem Th142: :: GLIB_006:138

for G2 being _Graph
for v1 being set
for e being object
for 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

proof end;

theorem :: GLIB_006:139

for G being non _trivial _Graph
for v1 being Vertex of G
for 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

proof end;

theorem :: GLIB_006:140

for G being non _trivial _Graph
for v1, e being object
for 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

proof end;

:: 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 Th145: :: GLIB_006:141

for G2 being _Graph
for v1 being Vertex of G2
for 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

proof end;

theorem Th146: :: GLIB_006:142

for G2 being _Graph
for v1, e being object
for 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

proof end;

theorem Th147: :: GLIB_006:143

for G2 being _Graph
for v1 being Vertex of G2
for 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
not G1 is _trivial

proof end;

theorem Th148: :: GLIB_006:144

for G2 being _Graph
for v1, e being object
for 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
not G1 is _trivial

proof end;

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;

coherence
for b₁ being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b₁ is _trivial

proof end;

cluster -> non _trivial for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;

coherence
for b₁ being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b₁ is _trivial

proof end;

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;

coherence
for b₁ being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds b₁ is complete

proof end;

cluster -> complete for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;

coherence
for b₁ being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds b₁ is complete

proof end;

end;

registration

let G be loopless _Graph;
let v1, e, v2 be object ;

cluster -> loopless for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is loopless

proof end;

end;

registration

let G be non-Dmulti _Graph;
let v1, e, v2 be object ;

cluster -> non-Dmulti for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is non-Dmulti

proof end;

end;

registration

let G be non-multi _Graph;
let v1, e, v2 be object ;

cluster -> non-multi for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is non-multi

proof end;

end;

registration

let G be Dsimple _Graph;
let v1, e, v2 be object ;

cluster -> Dsimple for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is Dsimple ;

end;

registration

let G be simple _Graph;
let v1, e, v2 be object ;

cluster -> simple for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is simple ;

end;

theorem Th149: :: GLIB_006:145

for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for 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 V5() ) or not v2 in W .vertices() ) holds
W is Walk of G2

proof end;

theorem Th150: :: GLIB_006:146

for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2
for 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 V5() ) or not v1 in W .vertices() ) holds
W is Walk of G2

proof end;

theorem Th151: :: GLIB_006:147

for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2
for 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()

proof end;

registration

let G be connected _Graph;
let v1, e, v2 be object ;

cluster -> connected for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is connected

proof end;

end;

registration

let G be non connected _Graph;
let v1, e, v2 be object ;

cluster -> non connected for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds not b₁ is connected

proof end;

end;

registration

let G be acyclic _Graph;
let v1, e, v2 be object ;

cluster -> acyclic for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is acyclic

proof end;

end;

registration

let G be Tree-like _Graph;
let v1, e, v2 be object ;

cluster -> Tree-like for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is Tree-like ;

end;

theorem Th152: :: GLIB_006:148

for G2 being _Graph
for v1 being Vertex of G2
for 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 & not G2 is _trivial holds
not G1 is complete

proof end;

theorem Th153: :: GLIB_006:149

for G2 being _Graph
for v1, e being object
for 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 & not G2 is _trivial holds
not G1 is complete

proof end;

registration

let G be non complete _Graph;
let v1, e, v2 be object ;

cluster -> non complete for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds not b₁ is complete

proof end;

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;

coherence
for b₁ being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b₁ is complete

proof end;

cluster -> non complete for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;

coherence
for b₁ being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b₁ is complete

proof end;

end;

theorem :: GLIB_006:150

for G2 being _Graph
for v1 being Vertex of G2
for 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 )

proof end;

theorem :: GLIB_006:151

for G2 being _Graph
for v1, e being object
for 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 )

proof end;

theorem :: GLIB_006:152

for G2 being _finite _Graph
for v1 being Vertex of G2
for 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 )

proof end;

theorem :: GLIB_006:153

for G2 being _finite _Graph
for v1, e being object
for 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 )

proof end;

registration

let G be _finite _Graph;
let v1, e, v2 be object ;

cluster -> _finite for addAdjVertex of G,v1,e,v2;

coherence
for b₁ being addAdjVertex of G,v1,e,v2 holds b₁ is _finite

proof end;

end;