:: by Sebastian Koch

::

:: Received June 29, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

:: into ABIAN ?

:: into ABIAN ?

:: into NAT_D ?

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

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

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

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 ?

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

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;

end;
let f, g be FinSequence of D;

let n be Nat;

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

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

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;

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;

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

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

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;

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;

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

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;

coherence

for b_{1} being Subgraph of G holds b_{1} is non-Dmulti

end;
coherence

for b

proof end;

:: into GLIB_000 ?

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

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 )

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 = {} )

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

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

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

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

( 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;

coherence

for b_{1} being Walk of G st b_{1} is closed & b_{1} is Trail-like & not b_{1} is trivial holds

b_{1} is Circuit-like
by GLIB_001:def 30;

coherence

for b_{1} being Walk of G st b_{1} is closed & b_{1} is Path-like & not b_{1} is trivial holds

b_{1} is Cycle-like
by GLIB_001:def 31;

end;
coherence

for b

b

coherence

for b

b

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

:: into GLIB_001 ?

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

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 ?

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

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 ?

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

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 ?

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

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

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

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

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

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

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;

( ( W2 is_odd_substring_of W1, 0 implies ex b_{1} being odd Element of NAT st

( b_{1} <= len W1 & ex k being even Nat st

( b_{1} = 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_{1} being odd Element of NAT st b_{1} = len W1 ) )

for b_{1}, b_{2} being odd Element of NAT holds

( ( W2 is_odd_substring_of W1, 0 & b_{1} <= len W1 & ex k being even Nat st

( b_{1} = 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_{2} <= len W1 & ex k being even Nat st

( b_{2} = 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_{1} = b_{2} ) & ( not W2 is_odd_substring_of W1, 0 & b_{1} = len W1 & b_{2} = len W1 implies b_{1} = b_{2} ) )

for b_{1} being odd Element of NAT holds verum
;

( ( W2 is_odd_substring_of W1, 0 implies ex b_{1} being odd Element of NAT st

( b_{1} <= len W1 & ex k being even Nat st

( b_{1} = 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_{1} being odd Element of NAT st b_{1} = len W1 ) )

for b_{1}, b_{2} being odd Element of NAT holds

( ( W2 is_odd_substring_of W1, 0 & b_{1} <= len W1 & ex k being even Nat st

( b_{1} = 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_{2} <= len W1 & ex k being even Nat st

( b_{2} = 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_{1} = b_{2} ) & ( not W2 is_odd_substring_of W1, 0 & b_{1} = len W1 & b_{2} = len W1 implies b_{1} = b_{2} ) )

for b_{1} being odd Element of NAT holds verum
;

end;
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 ( 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;

( ( W2 is_odd_substring_of W1, 0 implies ex b

( b

( b

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

proof end;

uniqueness for b

( ( W2 is_odd_substring_of W1, 0 & b

( b

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

( b

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

proof end;

consistency for b

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 ( 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;

( ( W2 is_odd_substring_of W1, 0 implies ex b

( b

( b

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

proof end;

uniqueness for b

( ( W2 is_odd_substring_of W1, 0 & b

( b

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

( b

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

proof end;

consistency for b

:: deftheorem Def3 defines .findFirstVertex GLIB_006:def 3 :

for G being _Graph

for W1, W2 being Walk of G

for b_{4} being odd Element of NAT holds

( ( W2 is_odd_substring_of W1, 0 implies ( b_{4} = W1 .findFirstVertex W2 iff ( b_{4} <= len W1 & ex k being even Nat st

( b_{4} = 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_{4} = W1 .findFirstVertex W2 iff b_{4} = len W1 ) ) );

for G being _Graph

for W1, W2 being Walk of G

for b

( ( W2 is_odd_substring_of W1, 0 implies ( b

( b

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

:: deftheorem Def4 defines .findLastVertex GLIB_006:def 4 :

for G being _Graph

for W1, W2 being Walk of G

for b_{4} being odd Element of NAT holds

( ( W2 is_odd_substring_of W1, 0 implies ( b_{4} = W1 .findLastVertex W2 iff ( b_{4} <= len W1 & ex k being even Nat st

( b_{4} = 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_{4} = W1 .findLastVertex W2 iff b_{4} = len W1 ) ) );

for G being _Graph

for W1, W2 being Walk of G

for b

( ( W2 is_odd_substring_of W1, 0 implies ( b

( b

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

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

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;

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 )

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

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;

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_{1} being Walk of G holds verum;

;

end;
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 ((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;

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

;

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

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 ;

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_{1} being Walk of G holds verum;

;

end;
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 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;

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

;

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

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 ;

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_{1} being Walk of G holds verum;

;

end;
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 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;

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

;

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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 )

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 )

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 )

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 ?

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

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

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

v2 in G .reachableFrom v1

proof end;

:: into GLIB_002 ?

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

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 )

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;

coherence

for b_{1} being Vertex of G st b_{1} is isolated holds

not b_{1} is cut-vertex

end;
coherence

for b

not b

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

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 ?

:: into CHORD ?

registration

for b_{1} being _Graph st b_{1} is complete holds

b_{1} is connected
end;

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

coherence for b

b

proof end;

registration

ex b_{1} being _Graph st

( not b_{1} is non-Dmulti & not b_{1} is non-multi & not b_{1} is loopless & not b_{1} is Dsimple & not b_{1} is simple & not b_{1} is acyclic & not b_{1} is finite )
end;

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

( not b

proof end;

definition

let G be _Graph;

ex b_{1} being Subset of (the_Vertices_of G) st

for v being object holds

( v in b_{1} iff ex w being Vertex of G st

( v = w & w is endvertex ) )

for b_{1}, b_{2} being Subset of (the_Vertices_of G) st ( for v being object holds

( v in b_{1} iff ex w being Vertex of G st

( v = w & w is endvertex ) ) ) & ( for v being object holds

( v in b_{2} iff ex w being Vertex of G st

( v = w & w is endvertex ) ) ) holds

b_{1} = b_{2}

end;
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 for v being object holds

( v in it iff ex w being Vertex of G st

( v = w & w is endvertex ) );

ex b

for v being object holds

( v in b

( v = w & w is endvertex ) )

proof end;

uniqueness for b

( v in b

( v = w & w is endvertex ) ) ) & ( for v being object holds

( v in b

( v = w & w is endvertex ) ) ) holds

b

proof end;

:: deftheorem Def8 defines Endvertices GLIB_006:def 8 :

for G being _Graph

for b_{2} being Subset of (the_Vertices_of G) holds

( b_{2} = Endvertices G iff for v being object holds

( v in b_{2} iff ex w being Vertex of G st

( v = w & w is endvertex ) ) );

for G being _Graph

for b

( b

( v in b

( v = w & w is endvertex ) ) );

:: analogue to GLIB_000:def 32

definition

let G be _Graph;

ex b_{1} being _Graph st

( the_Vertices_of G c= the_Vertices_of b_{1} & the_Edges_of G c= the_Edges_of b_{1} & ( for e being set st e in the_Edges_of G holds

( (the_Source_of G) . e = (the_Source_of b_{1}) . e & (the_Target_of G) . e = (the_Target_of b_{1}) . e ) ) )

end;
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 ( 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 ) ) );

ex b

( the_Vertices_of G c= the_Vertices_of b

( (the_Source_of G) . e = (the_Source_of b

proof end;

:: deftheorem Def9 defines Supergraph GLIB_006:def 9 :

for G, b_{2} being _Graph holds

( b_{2} is Supergraph of G iff ( the_Vertices_of G c= the_Vertices_of b_{2} & the_Edges_of G c= the_Edges_of b_{2} & ( for e being set st e in the_Edges_of G holds

( (the_Source_of G) . e = (the_Source_of b_{2}) . e & (the_Target_of G) . e = (the_Target_of b_{2}) . e ) ) ) );

for G, b

( b

( (the_Source_of G) . e = (the_Source_of b

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

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

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

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 )

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

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

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

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;

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

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

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 )

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 )

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

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

for G1 being finite Supergraph of G2 holds

( G2 .order() <= G1 .order() & G2 .size() <= G1 .size() )

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 trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( 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 ) )

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 trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( 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;

coherence

for b_{1} being Supergraph of G holds not b_{1} is trivial

end;
coherence

for b

proof end;

registration

let G be non non-Dmulti _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is non-Dmulti

end;
coherence

for b

proof end;

registration

let G be non non-multi _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is non-multi

end;
coherence

for b

proof end;

registration

let G be non loopless _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is loopless

end;
coherence

for b

proof end;

registration

let G be non Dsimple _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is Dsimple

end;
coherence

for b

proof end;

registration

let G be non simple _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is simple

end;
coherence

for b

proof end;

registration

let G be non acyclic _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is acyclic

end;
coherence

for b

proof end;

registration

let G be non finite _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is finite

end;
coherence

for b

proof end;

definition

let G be _Graph;

let V be set ;

ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = (the_Vertices_of G) \/ V & the_Edges_of b_{1} = the_Edges_of G & the_Source_of b_{1} = the_Source_of G & the_Target_of b_{1} = the_Target_of G )

end;
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 ( 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 );

ex b

( the_Vertices_of b

proof end;

:: deftheorem Def10 defines addVertices GLIB_006:def 10 :

for G being _Graph

for V being set

for b_{3} being Supergraph of G holds

( b_{3} is addVertices of G,V iff ( the_Vertices_of b_{3} = (the_Vertices_of G) \/ V & the_Edges_of b_{3} = the_Edges_of G & the_Source_of b_{3} = the_Source_of G & the_Target_of b_{3} = the_Target_of G ) );

for G being _Graph

for V being set

for b

( b

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 )

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

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

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

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

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

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)

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 )

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

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 )

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 )

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 )

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 ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is non-Dmulti

end;
let V be set ;

coherence

for b

proof end;

registration

let G be non-multi _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is non-multi

end;
let V be set ;

coherence

for b

proof end;

registration

let G be loopless _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is loopless

end;
let V be set ;

coherence

for b

proof end;

registration

let G be Dsimple _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is Dsimple
;

end;
let V be set ;

coherence

for b

registration

let G be Dsimple _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is Dsimple
;

end;
let V be set ;

coherence

for b

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 W is trivial )

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 W is trivial )

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

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 ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is acyclic

end;
let V be set ;

coherence

for b

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

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

:: because non chordal existence will be proven with cycle graphs

registration

let G be chordal _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is chordal
by Th96;

end;
let V be set ;

coherence

for b

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;

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;

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

proof end;

registration

let G be _Graph;

coherence

for b_{1} being addVertex of G,(the_Vertices_of G) holds

( not b_{1} is trivial & not b_{1} is connected & not b_{1} is complete )

end;
coherence

for b

( not b

proof end;

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

:: of certain graphs

:: of certain graphs

registration

ex b_{1} being _Graph st

( not b_{1} is trivial & not b_{1} is connected & not b_{1} is complete )
end;

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

existence ex b

( not b

proof end;

registration

let G be non connected _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds not b_{1} is connected

end;
let V be set ;

coherence

for b

proof 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.

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

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

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

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

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 ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is finite

end;
let V be finite set ;

coherence

for b

proof end;

registration

let G be finite _Graph;

let v be object ;

coherence

for b_{1} being addVertex of G,v holds b_{1} is finite
;

end;
let v be object ;

coherence

for b

registration

let G be _Graph;

let V be non finite set ;

coherence

for b_{1} being addVertices of G,V holds not b_{1} is finite

end;
let V be non finite set ;

coherence

for b

proof end;

:: we explicitly add an edge only if it is not used already

:: to ensure getting a Supergraph

:: to ensure getting a Supergraph

definition

let G be _Graph;

let v1, e, v2 be object ;

( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = the_Vertices_of G & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (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_{1} being Supergraph of G st b_{1} == G ) )

for b_{1} being Supergraph of G holds verum
;

end;
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 ( 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;

( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b

( the_Vertices_of b

proof end;

consistency for b

:: deftheorem Def11 defines addEdge GLIB_006:def 11 :

for G being _Graph

for v1, e, v2 being object

for b_{5} 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_{5} is addEdge of G,v1,e,v2 iff ( the_Vertices_of b_{5} = the_Vertices_of G & the_Edges_of b_{5} = (the_Edges_of G) \/ {e} & the_Source_of b_{5} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{5} = (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_{5} is addEdge of G,v1,e,v2 iff b_{5} == G ) ) );

for G being _Graph

for v1, e, v2 being object

for b

( ( v1 in the_Vertices_of G & v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b

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 )

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

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

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

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

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

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

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 )

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

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

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 ;

coherence

for b_{1} being addEdge of G,v1,e,v2 holds b_{1} is trivial

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be connected _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addEdge of G,v1,e,v2 holds b_{1} is connected

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be complete _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addEdge of G,v1,e,v2 holds b_{1} is complete

end;
let v1, e, v2 be object ;

coherence

for b

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

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

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 ;

coherence

for b_{1} being addEdge of G,v1,e,v2 holds b_{1} is finite

end;
let v1, e, v2 be object ;

coherence

for b

proof 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

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

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;

coherence

for b_{1} being addEdge of G,v, the_Edges_of G,v holds not b_{1} is loopless

end;
let v be Vertex of G;

coherence

for b

proof 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

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

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

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

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

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

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

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

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

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

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 ;

( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v2} & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (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_{1} being Supergraph of G st

( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v1} & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (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_{1} being Supergraph of G st b_{1} == G ) )

for b_{1} 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_{1} = (the_Vertices_of G) \/ {v2} & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (the_Target_of G) +* (e .--> v2) iff ( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v1} & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (the_Target_of G) +* (e .--> v2) ) )
;

end;
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 ( 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;

( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ex b

( the_Vertices_of b

( the_Vertices_of b

proof end;

consistency for b

( the_Vertices_of b

:: deftheorem Def12 defines addAdjVertex GLIB_006:def 12 :

for G being _Graph

for v1, e, v2 being object

for b_{5} 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_{5} is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b_{5} = (the_Vertices_of G) \/ {v2} & the_Edges_of b_{5} = (the_Edges_of G) \/ {e} & the_Source_of b_{5} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{5} = (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_{5} is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b_{5} = (the_Vertices_of G) \/ {v1} & the_Edges_of b_{5} = (the_Edges_of G) \/ {e} & the_Source_of b_{5} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{5} = (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_{5} is addAdjVertex of G,v1,e,v2 iff b_{5} == G ) ) );

for G being _Graph

for v1, e, v2 being object

for b

( ( v1 in the_Vertices_of G & not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b

definition

let G be _Graph;

let v1 be Vertex of G;

let e, v2 be object ;

for b_{1} being Supergraph of G holds

( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b_{1} is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v2} & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b_{1} is addAdjVertex of G,v1,e,v2 iff b_{1} == G ) ) )
by Def12;

consistency

for b_{1} being Supergraph of G holds verum
;

end;
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 ( 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;

for b

( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b

consistency

for b

:: 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_{5} being Supergraph of G holds

( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b_{5} is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b_{5} = (the_Vertices_of G) \/ {v2} & the_Edges_of b_{5} = (the_Edges_of G) \/ {e} & the_Source_of b_{5} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{5} = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v2 in the_Vertices_of G or e in the_Edges_of G ) implies ( b_{5} is addAdjVertex of G,v1,e,v2 iff b_{5} == G ) ) );

for G being _Graph

for v1 being Vertex of G

for e, v2 being object

for b

( ( not v2 in the_Vertices_of G & not e in the_Edges_of G implies ( b

definition

let G be _Graph;

let v1, e be object ;

let v2 be Vertex of G;

for b_{1} being Supergraph of G holds

( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b_{1} is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v1} & the_Edges_of b_{1} = (the_Edges_of G) \/ {e} & the_Source_of b_{1} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{1} = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v1 in the_Vertices_of G or e in the_Edges_of G ) implies ( b_{1} is addAdjVertex of G,v1,e,v2 iff b_{1} == G ) ) )
by Def12;

consistency

for b_{1} being Supergraph of G holds verum
;

end;
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 ( 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;

for b

( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b

consistency

for b

:: 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_{5} being Supergraph of G holds

( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b_{5} is addAdjVertex of G,v1,e,v2 iff ( the_Vertices_of b_{5} = (the_Vertices_of G) \/ {v1} & the_Edges_of b_{5} = (the_Edges_of G) \/ {e} & the_Source_of b_{5} = (the_Source_of G) +* (e .--> v1) & the_Target_of b_{5} = (the_Target_of G) +* (e .--> v2) ) ) ) & ( ( v1 in the_Vertices_of G or e in the_Edges_of G ) implies ( b_{5} is addAdjVertex of G,v1,e,v2 iff b_{5} == G ) ) );

for G being _Graph

for v1, e being object

for v2 being Vertex of G

for b

( ( not v1 in the_Vertices_of G & not e in the_Edges_of G implies ( b

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

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

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

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

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

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

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

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

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 )

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 )

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

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

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

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)

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

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

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

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

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)

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

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

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

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

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;

coherence

for b_{1} being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b_{1} is trivial

for b_{1} being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b_{1} is trivial

end;
let v be Vertex of G;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be trivial _Graph;

let v be Vertex of G;

coherence

for b_{1} being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds b_{1} is complete

for b_{1} being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds b_{1} is complete

end;
let v be Vertex of G;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be loopless _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is loopless

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be non-Dmulti _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is non-Dmulti

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be non-multi _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is non-multi

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be Dsimple _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is Dsimple
;

end;
let v1, e, v2 be object ;

coherence

for b

registration

let G be simple _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is simple
;

end;
let v1, e, v2 be object ;

coherence

for b

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() & not W is trivial ) or not v2 in W .vertices() ) holds

W is Walk of G2

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() & not W is trivial ) 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() & not W is trivial ) or not v1 in W .vertices() ) holds

W is Walk of G2

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() & not W is trivial ) 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()

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 ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is connected

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be non connected _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds not b_{1} is connected

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be acyclic _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is acyclic

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be Tree-like _Graph;

let v1, e, v2 be object ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is Tree-like
;

end;
let v1, e, v2 be object ;

coherence

for b

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

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

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 ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds not b_{1} is complete

end;
let v1, e, v2 be object ;

coherence

for b

proof end;

registration

let G be non trivial _Graph;

let v be Vertex of G;

coherence

for b_{1} being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b_{1} is complete

for b_{1} being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b_{1} is complete

end;
let v be Vertex of G;

coherence

for b

proof end;

coherence for b

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

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 )

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 )

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 )

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 ;

coherence

for b_{1} being addAdjVertex of G,v1,e,v2 holds b_{1} is finite

end;
let v1, e, v2 be object ;

coherence

for b

proof end;