:: by Sebastian Koch

::

:: Received August 29, 2019

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

:: into XBOOLE_1 ?

Lm1: for R being Relation

for X being set holds (R | X) ~ = X |` (R ~)

proof end;

:: into RELAT_1 ?

::$CT

:: into FUNCT_1 ?

:: reformulation of FUNCT_1:113

:: into FUNCT_1 ?

:: reformulation of FUNCT_1:113

:: into FUNCT_1 ?

theorem :: GLIB_009:5

for f being one-to-one Function

for X being set holds

( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )

for X being set holds

( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )

proof end;

:: BEGIN into GLIB_000 ?

theorem Th6: :: GLIB_009:6

for G being _Graph

for e, x1, y1, x2, y2 being object st e DJoins x1,y1,G & e DJoins x2,y2,G holds

( x1 = x2 & y1 = y2 )

for e, x1, y1, x2, y2 being object st e DJoins x1,y1,G & e DJoins x2,y2,G holds

( x1 = x2 & y1 = y2 )

proof end;

registration

for b_{1} being _Graph st b_{1} is _trivial & b_{1} is non-Dmulti holds

b_{1} is non-multi

coherence

the_Edges_of G is trivial
end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] _trivial non-Dmulti -> non-multi for set ;

coherence for b

b

proof end;

let G be _trivial non-Dmulti _Graph;coherence

the_Edges_of G is trivial

proof end;

theorem Th7: :: GLIB_009:7

for G being _Graph

for X, Y being set

for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds

e DSJoins X,Y,G

for X, Y being set

for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds

e DSJoins X,Y,G

proof end;

theorem :: GLIB_009:8

for G being _trivial _Graph

for H being _Graph st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G holds

( H is _trivial & H is Subgraph of G )

for H being _Graph st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G holds

( H is _trivial & H is Subgraph of G )

proof end;

theorem Th10: :: GLIB_009:10

for G being _Graph

for X, Y being set

for e being object holds

( e SJoins X,Y,G iff e SJoins Y,X,G )

for X, Y being set

for e being object holds

( e SJoins X,Y,G iff e SJoins Y,X,G )

proof end;

theorem Th11: :: GLIB_009:11

for G being _Graph

for X, Y being set

for e being object holds

( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) )

for X, Y being set

for e being object holds

( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) )

proof end;

theorem :: GLIB_009:14

for G being _Graph

for v, w being object st v <> w holds

( G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) & G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) )

for v, w being object st v <> w holds

( G .edgesDBetween ({v},{w}) misses G .edgesDBetween ({w},{v}) & G .edgesBetween ({v},{w}) = (G .edgesDBetween ({v},{w})) \/ (G .edgesDBetween ({w},{v})) )

proof end;

theorem Th20: :: GLIB_009:20

for G being _Graph holds

( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )

( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )

proof end;

theorem Th21: :: GLIB_009:21

for G being _Graph holds

( G is loopless iff for v being object holds G .edgesDBetween ({v},{v}) = {} )

( G is loopless iff for v being object holds G .edgesDBetween ({v},{v}) = {} )

proof end;

registration

let G be loopless _Graph;

let v be object ;

coherence

G .edgesBetween ({v},{v}) is empty by Th20;

coherence

G .edgesDBetween ({v},{v}) is empty by Th21;

end;
let v be object ;

coherence

G .edgesBetween ({v},{v}) is empty by Th20;

coherence

G .edgesDBetween ({v},{v}) is empty by Th21;

theorem Th22: :: GLIB_009:22

for G being _Graph holds

( G is non-multi iff for v, w being object holds G .edgesBetween ({v},{w}) is trivial )

( G is non-multi iff for v, w being object holds G .edgesBetween ({v},{w}) is trivial )

proof end;

registration

let G be non-multi _Graph;

let v, w be object ;

coherence

G .edgesBetween ({v},{w}) is trivial by Th22;

end;
let v, w be object ;

coherence

G .edgesBetween ({v},{w}) is trivial by Th22;

theorem Th23: :: GLIB_009:23

for G being _Graph holds

( G is non-Dmulti iff for v, w being object holds G .edgesDBetween ({v},{w}) is trivial )

( G is non-Dmulti iff for v, w being object holds G .edgesDBetween ({v},{w}) is trivial )

proof end;

registration

let G be non-Dmulti _Graph;

let v, w be object ;

coherence

G .edgesDBetween ({v},{w}) is trivial by Th23;

end;
let v, w be object ;

coherence

G .edgesDBetween ({v},{w}) is trivial by Th23;

registration

let G be non _trivial _Graph;

coherence

for b_{1} being Subgraph of G st b_{1} is spanning holds

not b_{1} is _trivial

end;
coherence

for b

not b

proof end;

registration

let G be _Graph;

coherence

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

not b_{1} is endvertex

end;
coherence

for b

not b

proof end;

:: END into GLIB_000 ?

:: into GLIB_001 ?

:: into GLIB_001 ?

:: into GLIB_001 ?

:: into GLIB_001

registration

let G be _Graph;

let W be V5() Walk of G;

coherence

( W .edges() is empty & W .edges() is trivial )

end;
let W be V5() Walk of G;

coherence

( W .edges() is empty & W .edges() is trivial )

proof end;

:: into GLIB_001 ?

registration
end;

:: into GLIB_001 ?

theorem :: GLIB_009:26

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds

W1 = W2

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds

W1 = W2

proof end;

:: into GLIB_001 ?

theorem :: GLIB_009:27

for G being _Graph

for p being FinSequence of the_Vertices_of G

for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds

q . n Joins p . n,p . (n + 1),G ) holds

ex W being Walk of G st

( W .vertexSeq() = p & W .edgeSeq() = q )

for p being FinSequence of the_Vertices_of G

for q being FinSequence of the_Edges_of G st len p = 1 + (len q) & ( for n being Element of NAT st 1 <= n & n + 1 <= len p holds

q . n Joins p . n,p . (n + 1),G ) holds

ex W being Walk of G st

( W .vertexSeq() = p & W .edgeSeq() = q )

proof end;

Lm2: for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 holds

( len W1 = len W2 iff W1 .length() = W2 .length() )

proof end;

:: into GLIB_001 ?

Lm3: for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds

len W1 = len W2

proof end;

:: into GLIB_001 ?

theorem Th29: :: GLIB_009:29

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2

for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

for W1 being Walk of G1

for W2 being Walk of G2

for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds

W1 . n = W2 . n

proof end;

:: into GLIB_001 ?

theorem Th30: :: GLIB_009:30

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds

( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds

( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )

proof end;

:: into GLIB_001 ?

theorem Th31: :: GLIB_009:31

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds

( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds

( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

proof end;

:: into GLIB_001 ?

:: in the case len W1 = 5, W1 could be the Path in a dipole visiting both

:: edges while W2 goes back on the same edge it came from

:: in the case len W1 = 5, W1 could be the Path in a dipole visiting both

:: edges while W2 goes back on the same edge it came from

theorem Th32: :: GLIB_009:32

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds

( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & len W1 <> 5 holds

( ( W1 is Path-like implies W2 is Path-like ) & ( W1 is Cycle-like implies W2 is Cycle-like ) )

proof end;

:: into GLIB_001 ?

:: into GLIB_001 ?

:: into GLIB_002 ?

theorem Th33: :: GLIB_009:33

for G1 being _Graph

for E being Subset of (the_Edges_of G1)

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E st G2 is connected holds

G1 is connected

for E being Subset of (the_Edges_of G1)

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E st G2 is connected holds

G1 is connected

proof end;

:: into GLIB_002 ?

theorem :: GLIB_009:34

:: into GLIB_002 ?

registration

let G1 be non connected _Graph;

let E be set ;

coherence

for b_{1} being removeEdges of G1,E holds not b_{1} is connected
by Th33;

end;
let E be set ;

coherence

for b

:: into GLIB_002 ?

theorem Th35: :: GLIB_009:35

for G1 being _Graph

for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) holds

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) holds

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

:: into GLIB_002 ?

theorem Th36: :: GLIB_009:36

for G1 being _Graph

for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) & G1 is connected holds

G2 is connected

for G2 being Subgraph of G1 st ( for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last() ) & G1 is connected holds

G2 is connected

proof end;

:: into GLIB_002 ?

theorem Th37: :: GLIB_009:37

for G1 being _Graph

for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds

G1 .componentSet() = G2 .componentSet()

for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds

G1 .componentSet() = G2 .componentSet()

proof end;

:: into GLIB_002 ?

theorem Th38: :: GLIB_009:38

for G1 being _Graph

for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds

G1 .numComponents() = G2 .numComponents()

for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds

G1 .numComponents() = G2 .numComponents()

proof end;

:: into CHORD ?

registration

let G be non complete _Graph;

coherence

for b_{1} being Subgraph of G st b_{1} is spanning holds

not b_{1} is complete

end;
coherence

for b

not b

proof end;

:: into GLIB_006 ?

theorem Th41: :: GLIB_009:41

for G2 being _Graph

for V being set

for G1 being addVertices of G2,V

for x, y being set

for e being object holds

( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )

for V being set

for G1 being addVertices of G2,V

for x, y being set

for e being object holds

( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )

proof end;

:: into GLIB_007 ?

:: into GLIB_007 ?

definition
end;

:: deftheorem Def1 defines plain GLIB_009:def 1 :

for G being _Graph holds

( G is plain iff dom G = _GraphSelectors );

for G being _Graph holds

( G is plain iff dom G = _GraphSelectors );

registration

let V be non empty set ;

let E be set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is plain

end;
let E be set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is plain

proof end;

registration

let G be _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is plain

not G .set (ELabelSelector,X) is plain

not G .set (VLabelSelector,X) is plain

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is plain

proof end;

coherence not G .set (ELabelSelector,X) is plain

proof end;

coherence not G .set (VLabelSelector,X) is plain

proof end;

:: existence clusters for plain graph modes

registration

let G be _Graph;

existence

ex b_{1} being Subgraph of G st b_{1} is plain

ex b_{1} being removeVertices of G,V st b_{1} is plain

ex b_{1} being inducedSubgraph of G,V,E st b_{1} is plain

end;
existence

ex b

proof end;

let V be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,(the_Vertices_of G) \ V,G .edgesBetween ((the_Vertices_of G) \ V);

existence ex b

proof end;

let E be set ;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,V,E;

existence ex b

proof end;

registration

let G be _Graph;

let E be set ;

ex b_{1} being removeEdges of G,E st b_{1} is plain

ex b_{1} being reverseEdgeDirections of G,E st b_{1} is plain

end;
let E be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;

existence ex b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for reverseEdgeDirections of G,E;

existence ex b

proof end;

registration

let G be _Graph;

let v be set ;

ex b_{1} being removeVertex of G,v st b_{1} is plain

end;
let v be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,(the_Vertices_of G) \ {v},G .edgesBetween ((the_Vertices_of G) \ {v});

existence ex b

proof end;

registration

let G be _Graph;

let e be set ;

ex b_{1} being removeEdge of G,e st b_{1} is plain

end;
let e be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};

existence ex b

proof end;

registration

let G be _Graph;

existence

ex b_{1} being Supergraph of G st b_{1} is plain

existence

ex b_{1} being addVertices of G,V st b_{1} is plain

end;
existence

ex b

proof end;

let V be set ;existence

ex b

proof end;

registration

let G be _Graph;

let v, e, w be object ;

existence

ex b_{1} being addEdge of G,v,e,w st b_{1} is plain

ex b_{1} being addAdjVertex of G,v,e,w st b_{1} is plain

end;
let v, e, w be object ;

existence

ex b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertex of G,v,e,w;

existence ex b

proof end;

registration

let G be _Graph;

let v be object ;

let V be set ;

ex b_{1} being addAdjVertexFromAll of G,v,V st b_{1} is plain

ex b_{1} being addAdjVertexToAll of G,v,V st b_{1} is plain

ex b_{1} being addAdjVertexAll of G,v,V st b_{1} is plain

end;
let v be object ;

let V be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexFromAll of G,v,V;

existence ex b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexToAll of G,v,V;

existence ex b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexAll of G,v,V;

existence ex b

proof end;

definition

let G be _Graph;

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

for e being object holds

( e in b_{1} iff ex v being object st e Joins v,v,G )

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

( e in b_{1} iff ex v being object st e Joins v,v,G ) ) & ( for e being object holds

( e in b_{2} iff ex v being object st e Joins v,v,G ) ) holds

b_{1} = b_{2}

end;
func G .loops() -> Subset of (the_Edges_of G) means :Def2: :: GLIB_009:def 2

for e being object holds

( e in it iff ex v being object st e Joins v,v,G );

existence for e being object holds

( e in it iff ex v being object st e Joins v,v,G );

ex b

for e being object holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

:: deftheorem Def2 defines .loops() GLIB_009:def 2 :

for G being _Graph

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

( b_{2} = G .loops() iff for e being object holds

( e in b_{2} iff ex v being object st e Joins v,v,G ) );

for G being _Graph

for b

( b

( e in b

theorem Th45: :: GLIB_009:45

for G being _Graph

for e being object holds

( e in G .loops() iff ex v being object st e DJoins v,v,G )

for e being object holds

( e in G .loops() iff ex v being object st e DJoins v,v,G )

proof end;

registration
end;

theorem :: GLIB_009:51

for G1 being _Graph

for E being set

for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

for E being set

for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:52

for G2 being _Graph

for V being set

for G1 being addVertices of G2,V holds G1 .loops() = G2 .loops()

for V being set

for G1 being addVertices of G2,V holds G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:53

for G2 being _Graph

for v1, e, v2 being object

for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds

G1 .loops() = G2 .loops()

for v1, e, v2 being object

for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds

G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:54

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 e in the_Edges_of G2 holds

G1 .loops() = (G2 .loops()) \/ {e}

for v being Vertex of G2

for e being object

for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2 holds

G1 .loops() = (G2 .loops()) \/ {e}

proof end;

theorem :: GLIB_009:55

for G2 being _Graph

for v1, e, v2 being object

for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .loops() = G2 .loops()

for v1, e, v2 being object

for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:56

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()

proof end;

theorem Th57: :: GLIB_009:57

for G being _Graph

for P being Path of G holds

( P .edges() misses G .loops() or ex v, e being object st

( e Joins v,v,G & P = G .walkOf (v,e,v) ) )

for P being Path of G holds

( P .edges() misses G .loops() or ex v, e being object st

( e Joins v,v,G & P = G .walkOf (v,e,v) ) )

proof end;

theorem Th59: :: GLIB_009:59

for G1, G2 being _Graph

for G3 being removeLoops of G1 holds

( G2 == G3 iff G2 is removeLoops of G1 ) by GLIB_006:16, GLIB_000:93;

for G3 being removeLoops of G1 holds

( G2 == G3 iff G2 is removeLoops of G1 ) by GLIB_006:16, GLIB_000:93;

registration

let G be _Graph;

coherence

for b_{1} being removeLoops of G holds b_{1} is loopless

ex b_{1} being removeLoops of G st b_{1} is plain

end;
coherence

for b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

existence ex b

proof end;

registration
end;

registration
end;

registration

let G be complete _Graph;

coherence

for b_{1} being removeLoops of G holds b_{1} is complete

end;
coherence

for b

proof end;

theorem Th61: :: GLIB_009:61

for G1 being _Graph

for G2 being removeLoops of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

for G2 being removeLoops of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th62: :: GLIB_009:62

for G1 being _Graph

for G2 being removeLoops of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for G2 being removeLoops of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

registration

let G be connected _Graph;

coherence

for b_{1} being removeLoops of G holds b_{1} is connected

end;
coherence

for b

proof end;

registration

let G be non connected _Graph;

for b_{1} being removeLoops of G holds not b_{1} is connected
;

end;
cluster -> non connected for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence for b

:: non chordal cluster after non chordal has been clustered with cycles

registration
end;

:: More theorems of this kind can be produced with other

:: subgraph modes. This particular example was needed

:: to show that the cut-vertex property prevails in graphs

:: with removed loops

:: subgraph modes. This particular example was needed

:: to show that the cut-vertex property prevails in graphs

:: with removed loops

theorem Th66: :: GLIB_009:66

for G1 being _Graph

for v being set

for G2 being removeLoops of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

for v being set

for G2 being removeLoops of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

proof end;

theorem Th67: :: GLIB_009:67

for G1 being _Graph

for G2 being removeLoops of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

for G2 being removeLoops of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem Th68: :: GLIB_009:68

for G1 being _Graph

for G2 being removeLoops of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

for G2 being removeLoops of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

proof end;

definition

let G be _Graph;

ex b_{1} being Equivalence_Relation of (the_Edges_of G) st

for e1, e2 being object holds

( [e1,e2] in b_{1} iff ex v1, v2 being object st

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) )

for b_{1}, b_{2} being Equivalence_Relation of (the_Edges_of G) st ( for e1, e2 being object holds

( [e1,e2] in b_{1} iff ex v1, v2 being object st

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) & ( for e1, e2 being object holds

( [e1,e2] in b_{2} iff ex v1, v2 being object st

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Equivalence_Relation of (the_Edges_of G) st

for e1, e2 being object holds

( [e1,e2] in b_{1} iff ex v1, v2 being object st

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )

for b_{1}, b_{2} being Equivalence_Relation of (the_Edges_of G) st ( for e1, e2 being object holds

( [e1,e2] in b_{1} iff ex v1, v2 being object st

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) & ( for e1, e2 being object holds

( [e1,e2] in b_{2} iff ex v1, v2 being object st

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) holds

b_{1} = b_{2}

end;
func EdgeAdjEqRel G -> Equivalence_Relation of (the_Edges_of G) means :Def3: :: GLIB_009:def 3

for e1, e2 being object holds

( [e1,e2] in it iff ex v1, v2 being object st

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) );

existence for e1, e2 being object holds

( [e1,e2] in it iff ex v1, v2 being object st

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) );

ex b

for e1, e2 being object holds

( [e1,e2] in b

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) )

proof end;

uniqueness for b

( [e1,e2] in b

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) & ( for e1, e2 being object holds

( [e1,e2] in b

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) holds

b

proof end;

func DEdgeAdjEqRel G -> Equivalence_Relation of (the_Edges_of G) means :Def4: :: GLIB_009:def 4

for e1, e2 being object holds

( [e1,e2] in it iff ex v1, v2 being object st

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) );

existence for e1, e2 being object holds

( [e1,e2] in it iff ex v1, v2 being object st

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) );

ex b

for e1, e2 being object holds

( [e1,e2] in b

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )

proof end;

uniqueness for b

( [e1,e2] in b

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) & ( for e1, e2 being object holds

( [e1,e2] in b

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) holds

b

proof end;

:: deftheorem Def3 defines EdgeAdjEqRel GLIB_009:def 3 :

for G being _Graph

for b_{2} being Equivalence_Relation of (the_Edges_of G) holds

( b_{2} = EdgeAdjEqRel G iff for e1, e2 being object holds

( [e1,e2] in b_{2} iff ex v1, v2 being object st

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) );

for G being _Graph

for b

( b

( [e1,e2] in b

( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) );

:: deftheorem Def4 defines DEdgeAdjEqRel GLIB_009:def 4 :

for G being _Graph

for b_{2} being Equivalence_Relation of (the_Edges_of G) holds

( b_{2} = DEdgeAdjEqRel G iff for e1, e2 being object holds

( [e1,e2] in b_{2} iff ex v1, v2 being object st

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) );

for G being _Graph

for b

( b

( [e1,e2] in b

( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) );

registration
end;

registration

let G be non edgeless _Graph;

coherence

not EdgeAdjEqRel G is empty ;

coherence

not DEdgeAdjEqRel G is empty ;

end;
coherence

not EdgeAdjEqRel G is empty ;

coherence

not DEdgeAdjEqRel G is empty ;

definition

let G be _Graph;

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

for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in b_{1} & ( for e9 being object st e9 Joins v,w,G & e9 in b_{1} holds

e9 = e ) )

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

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b_{1} & ( for e9 being object st e9 DJoins v,w,G & e9 in b_{1} holds

e9 = e ) )

end;
mode RepEdgeSelection of G -> Subset of (the_Edges_of G) means :Def5: :: GLIB_009:def 5

for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in it & ( for e9 being object st e9 Joins v,w,G & e9 in it holds

e9 = e ) );

existence for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in it & ( for e9 being object st e9 Joins v,w,G & e9 in it holds

e9 = e ) );

ex b

for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in b

e9 = e ) )

proof end;

mode RepDEdgeSelection of G -> Subset of (the_Edges_of G) means :Def6: :: GLIB_009:def 6

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in it & ( for e9 being object st e9 DJoins v,w,G & e9 in it holds

e9 = e ) );

existence for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in it & ( for e9 being object st e9 DJoins v,w,G & e9 in it holds

e9 = e ) );

ex b

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b

e9 = e ) )

proof end;

:: deftheorem Def5 defines RepEdgeSelection GLIB_009:def 5 :

for G being _Graph

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

( b_{2} is RepEdgeSelection of G iff for v, w, e0 being object st e0 Joins v,w,G holds

ex e being object st

( e Joins v,w,G & e in b_{2} & ( for e9 being object st e9 Joins v,w,G & e9 in b_{2} holds

e9 = e ) ) );

for G being _Graph

for b

( b

ex e being object st

( e Joins v,w,G & e in b

e9 = e ) ) );

:: deftheorem Def6 defines RepDEdgeSelection GLIB_009:def 6 :

for G being _Graph

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

( b_{2} is RepDEdgeSelection of G iff for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b_{2} & ( for e9 being object st e9 DJoins v,w,G & e9 in b_{2} holds

e9 = e ) ) );

for G being _Graph

for b

( b

ex e being object st

( e DJoins v,w,G & e in b

e9 = e ) ) );

registration

let G be edgeless _Graph;

coherence

for b_{1} being RepEdgeSelection of G holds b_{1} is empty

for b_{1} being RepDEdgeSelection of G holds b_{1} is empty

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let G be non edgeless _Graph;

coherence

for b_{1} being RepEdgeSelection of G holds not b_{1} is empty

for b_{1} being RepDEdgeSelection of G holds not b_{1} is empty

end;
coherence

for b

proof end;

coherence for b

proof end;

theorem Th72: :: GLIB_009:72

for G being _Graph

for E1 being RepDEdgeSelection of G ex E2 being RepEdgeSelection of G st E2 c= E1

for E1 being RepDEdgeSelection of G ex E2 being RepEdgeSelection of G st E2 c= E1

proof end;

theorem Th73: :: GLIB_009:73

for G being _Graph

for E2 being RepEdgeSelection of G ex E1 being RepDEdgeSelection of G st E2 c= E1

for E2 being RepEdgeSelection of G ex E1 being RepDEdgeSelection of G st E2 c= E1

proof end;

theorem Th78: :: GLIB_009:78

for G1 being _Graph

for G2 being Subgraph of G1

for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepEdgeSelection of G2

for G2 being Subgraph of G1

for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepEdgeSelection of G2

proof end;

theorem Th79: :: GLIB_009:79

for G1 being _Graph

for G2 being Subgraph of G1

for E being RepDEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepDEdgeSelection of G2

for G2 being Subgraph of G1

for E being RepDEdgeSelection of G1 st E c= the_Edges_of G2 holds

E is RepDEdgeSelection of G2

proof end;

theorem Th80: :: GLIB_009:80

for G1 being _Graph

for G2 being Subgraph of G1

for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

for G2 being Subgraph of G1

for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

proof end;

theorem Th81: :: GLIB_009:81

for G1 being _Graph

for G2 being Subgraph of G1

for E2 being RepDEdgeSelection of G2 ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

for G2 being Subgraph of G1

for E2 being RepDEdgeSelection of G2 ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

proof end;

theorem Th82: :: GLIB_009:82

for G1 being _Graph

for E1 being RepEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds E1 = E2

for E1 being RepEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds E1 = E2

proof end;

theorem Th83: :: GLIB_009:83

for G1 being _Graph

for E1 being RepDEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepDEdgeSelection of G2 holds E1 = E2

for E1 being RepDEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepDEdgeSelection of G2 holds E1 = E2

proof end;

theorem Th84: :: GLIB_009:84

for G1 being _Graph

for E1 being RepDEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds

( E2 c= E1 & E2 is RepEdgeSelection of G1 )

for E1 being RepDEdgeSelection of G1

for G2 being inducedSubgraph of G1, the_Vertices_of G1,E1

for E2 being RepEdgeSelection of G2 holds

( E2 c= E1 & E2 is RepEdgeSelection of G1 )

proof end;

theorem Th85: :: GLIB_009:85

for G being _Graph

for E1, E2 being RepEdgeSelection of G ex f being one-to-one Function st

( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e Joins v,w,G iff f . e Joins v,w,G ) ) )

for E1, E2 being RepEdgeSelection of G ex f being one-to-one Function st

( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e Joins v,w,G iff f . e Joins v,w,G ) ) )

proof end;

theorem Th87: :: GLIB_009:87

for G being _Graph

for E1, E2 being RepDEdgeSelection of G ex f being one-to-one Function st

( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )

for E1, E2 being RepDEdgeSelection of G ex f being one-to-one Function st

( dom f = E1 & rng f = E2 & ( for e, v, w being object st e in E1 holds

( e DJoins v,w,G iff f . e DJoins v,w,G ) ) )

proof end;

definition

let G be _Graph;

ex b_{1} being Subgraph of G ex E being RepEdgeSelection of G st b_{1} is inducedSubgraph of G, the_Vertices_of G,E

ex b_{1} being Subgraph of G ex E being RepDEdgeSelection of G st b_{1} is inducedSubgraph of G, the_Vertices_of G,E

end;
mode removeParallelEdges of G -> Subgraph of G means :Def7: :: GLIB_009:def 7

ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;

existence ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;

ex b

proof end;

mode removeDParallelEdges of G -> Subgraph of G means :Def8: :: GLIB_009:def 8

ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;

existence ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;

ex b

proof end;

:: deftheorem Def7 defines removeParallelEdges GLIB_009:def 7 :

for G being _Graph

for b_{2} being Subgraph of G holds

( b_{2} is removeParallelEdges of G iff ex E being RepEdgeSelection of G st b_{2} is inducedSubgraph of G, the_Vertices_of G,E );

for G being _Graph

for b

( b

:: deftheorem Def8 defines removeDParallelEdges GLIB_009:def 8 :

for G being _Graph

for b_{2} being Subgraph of G holds

( b_{2} is removeDParallelEdges of G iff ex E being RepDEdgeSelection of G st b_{2} is inducedSubgraph of G, the_Vertices_of G,E );

for G being _Graph

for b

( b

registration

let G be _Graph;

coherence

for b_{1} being removeParallelEdges of G holds

( b_{1} is spanning & b_{1} is non-multi )

for b_{1} being removeDParallelEdges of G holds

( b_{1} is spanning & b_{1} is non-Dmulti )

ex b_{1} being removeParallelEdges of G st b_{1} is plain

ex b_{1} being removeDParallelEdges of G st b_{1} is plain

end;
coherence

for b

( b

proof end;

coherence for b

( b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for removeParallelEdges of G;

existence ex b

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for removeDParallelEdges of G;

existence ex b

proof end;

registration

let G be loopless _Graph;

coherence

for b_{1} being removeParallelEdges of G holds b_{1} is simple
;

coherence

for b_{1} being removeDParallelEdges of G holds b_{1} is Dsimple
;

end;
coherence

for b

coherence

for b

theorem :: GLIB_009:89

for G1 being non-multi _Graph

for G2 being _Graph holds

( G1 == G2 iff G2 is removeParallelEdges of G1 )

for G2 being _Graph holds

( G1 == G2 iff G2 is removeParallelEdges of G1 )

proof end;

theorem :: GLIB_009:90

for G1 being non-Dmulti _Graph

for G2 being _Graph holds

( G1 == G2 iff G2 is removeDParallelEdges of G1 )

for G2 being _Graph holds

( G1 == G2 iff G2 is removeDParallelEdges of G1 )

proof end;

theorem Th91: :: GLIB_009:91

for G1, G2 being _Graph

for G3 being removeParallelEdges of G1 st G1 == G2 holds

G3 is removeParallelEdges of G2

for G3 being removeParallelEdges of G1 st G1 == G2 holds

G3 is removeParallelEdges of G2

proof end;

theorem :: GLIB_009:92

for G1, G2 being _Graph

for G3 being removeDParallelEdges of G1 st G1 == G2 holds

G3 is removeDParallelEdges of G2

for G3 being removeDParallelEdges of G1 st G1 == G2 holds

G3 is removeDParallelEdges of G2

proof end;

theorem Th93: :: GLIB_009:93

for G1, G2 being _Graph

for G3 being removeParallelEdges of G1 st G2 == G3 holds

G2 is removeParallelEdges of G1

for G3 being removeParallelEdges of G1 st G2 == G3 holds

G2 is removeParallelEdges of G1

proof end;

theorem :: GLIB_009:94

for G1, G2 being _Graph

for G3 being removeDParallelEdges of G1 st G2 == G3 holds

G2 is removeDParallelEdges of G1

for G3 being removeDParallelEdges of G1 st G2 == G3 holds

G2 is removeDParallelEdges of G1

proof end;

theorem Th95: :: GLIB_009:95

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for G3 being removeParallelEdges of G2 holds G3 is removeParallelEdges of G1

for G2 being removeDParallelEdges of G1

for G3 being removeParallelEdges of G2 holds G3 is removeParallelEdges of G1

proof end;

theorem Th96: :: GLIB_009:96

for G1 being _Graph

for G2 being removeDParallelEdges of G1 ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2

for G2 being removeDParallelEdges of G1 ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2

proof end;

theorem Th97: :: GLIB_009:97

for G1 being _Graph

for G3 being removeParallelEdges of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeParallelEdges of G2

for G3 being removeParallelEdges of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeParallelEdges of G2

proof end;

registration

let G be complete _Graph;

coherence

for b_{1} being removeParallelEdges of G holds b_{1} is complete

for b_{1} being removeDParallelEdges of G holds b_{1} is complete

end;
coherence

for b

proof end;

coherence for b

proof end;

theorem Th98: :: GLIB_009:98

for G1 being _Graph

for G2 being removeParallelEdges of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()

for G2 being removeParallelEdges of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()

proof end;

Lm4: for G1 being _Graph

for G2 being removeParallelEdges of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th99: :: GLIB_009:99

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()

for G2 being removeDParallelEdges of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()

proof end;

Lm5: for G1 being _Graph

for G2 being removeDParallelEdges of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th100: :: GLIB_009:100

for G1 being _Graph

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

theorem Th101: :: GLIB_009:101

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

registration

let G be connected _Graph;

coherence

for b_{1} being removeParallelEdges of G holds b_{1} is connected

for b_{1} being removeDParallelEdges of G holds b_{1} is connected

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let G be non connected _Graph;

coherence

for b_{1} being removeParallelEdges of G holds not b_{1} is connected

for b_{1} being removeDParallelEdges of G holds not b_{1} is connected

end;
coherence

for b

proof end;

coherence for b

proof end;

theorem :: GLIB_009:102

for G1 being _Graph

for G2 being removeParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()

for G2 being removeParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem :: GLIB_009:103

for G1 being _Graph

for G2 being removeDParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()

for G2 being removeDParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem Th104: :: GLIB_009:104

for G1 being _Graph

for G2 being removeParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()

for G2 being removeParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem :: GLIB_009:105

for G1 being _Graph

for G2 being removeDParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()

for G2 being removeDParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem Th106: :: GLIB_009:106

for G1 being _Graph

for G2 being removeParallelEdges of G1 holds

( G1 is chordal iff G2 is chordal )

for G2 being removeParallelEdges of G1 holds

( G1 is chordal iff G2 is chordal )

proof end;

theorem Th107: :: GLIB_009:107

for G1 being _Graph

for G2 being removeDParallelEdges of G1 holds

( G1 is chordal iff G2 is chordal )

for G2 being removeDParallelEdges of G1 holds

( G1 is chordal iff G2 is chordal )

proof end;

:: non chordal cluster after non chordal has been clustered with cycles

registration

let G be chordal _Graph;

coherence

for b_{1} being removeParallelEdges of G holds b_{1} is chordal
by Th106;

coherence

for b_{1} being removeDParallelEdges of G holds b_{1} is chordal
by Th107;

end;
coherence

for b

coherence

for b

:: for cut-vertex property, same as with removeLoops above

theorem Th108: :: GLIB_009:108

for G1 being _Graph

for v being set

for G2 being removeParallelEdges of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3

for v being set

for G2 being removeParallelEdges of G1

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3

proof end;

theorem Th109: :: GLIB_009:109

for G1 being _Graph

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem Th110: :: GLIB_009:110

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem Th111: :: GLIB_009:111

for G1 being _Graph

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

proof end;

theorem Th112: :: GLIB_009:112

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

proof end;

theorem Th113: :: GLIB_009:113

for G1 being _Graph

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

for G2 being removeParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

proof end;

theorem Th114: :: GLIB_009:114

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

for G2 being removeDParallelEdges of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

proof end;

:: Graphs with Loops and parallel Edges removed

definition

let G be _Graph;

ex b_{1} being Subgraph of G ex E being RepEdgeSelection of G st b_{1} is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())

ex b_{1} being Subgraph of G ex E being RepDEdgeSelection of G st b_{1} is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())

end;
mode SimpleGraph of G -> Subgraph of G means :Def9: :: GLIB_009:def 9

ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());

existence ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());

ex b

proof end;

mode DSimpleGraph of G -> Subgraph of G means :Def10: :: GLIB_009:def 10

ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());

existence ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());

ex b

proof end;

:: deftheorem Def9 defines SimpleGraph GLIB_009:def 9 :

for G being _Graph

for b_{2} being Subgraph of G holds

( b_{2} is SimpleGraph of G iff ex E being RepEdgeSelection of G st b_{2} is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );

for G being _Graph

for b

( b

:: deftheorem Def10 defines DSimpleGraph GLIB_009:def 10 :

for G being _Graph

for b_{2} being Subgraph of G holds

( b_{2} is DSimpleGraph of G iff ex E being RepDEdgeSelection of G st b_{2} is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );

for G being _Graph

for b

( b

theorem :: GLIB_009:115

for G1 being _Graph

for G2 being removeParallelEdges of G1

for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

for G2 being removeParallelEdges of G1

for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

proof end;

theorem :: GLIB_009:116

for G1 being _Graph

for G2 being removeDParallelEdges of G1

for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1

for G2 being removeDParallelEdges of G1

for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1

proof end;

theorem Th117: :: GLIB_009:117

for G1 being _Graph

for G2 being removeLoops of G1

for G3 being removeParallelEdges of G2 holds G3 is SimpleGraph of G1

for G2 being removeLoops of G1

for G3 being removeParallelEdges of G2 holds G3 is SimpleGraph of G1

proof end;

theorem Th118: :: GLIB_009:118

for G1 being _Graph

for G2 being removeLoops of G1

for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1

for G2 being removeLoops of G1

for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1

proof end;

theorem Th119: :: GLIB_009:119

for G1 being _Graph

for G3 being SimpleGraph of G1 ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2

for G3 being SimpleGraph of G1 ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2

proof end;

theorem Th120: :: GLIB_009:120

for G1 being _Graph

for G3 being DSimpleGraph of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2

for G3 being DSimpleGraph of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2

proof end;

theorem Th121: :: GLIB_009:121

for G1 being _Graph

for G2 being removeLoops of G1

for G3 being SimpleGraph of G1 holds G3 is removeParallelEdges of G2

for G2 being removeLoops of G1

for G3 being SimpleGraph of G1 holds G3 is removeParallelEdges of G2

proof end;

theorem Th122: :: GLIB_009:122

for G1 being _Graph

for G2 being removeLoops of G1

for G3 being DSimpleGraph of G1 holds G3 is removeDParallelEdges of G2

for G2 being removeLoops of G1

for G3 being DSimpleGraph of G1 holds G3 is removeDParallelEdges of G2

proof end;

theorem Th123: :: GLIB_009:123

for G1 being loopless _Graph

for G2 being _Graph holds

( G2 is SimpleGraph of G1 iff G2 is removeParallelEdges of G1 )

for G2 being _Graph holds

( G2 is SimpleGraph of G1 iff G2 is removeParallelEdges of G1 )

proof end;

theorem :: GLIB_009:124

for G1 being loopless _Graph

for G2 being _Graph holds

( G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1 )

for G2 being _Graph holds

( G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1 )

proof end;

theorem :: GLIB_009:125

for G1 being non-multi _Graph

for G2 being _Graph holds

( G2 is SimpleGraph of G1 iff G2 is removeLoops of G1 )

for G2 being _Graph holds

( G2 is SimpleGraph of G1 iff G2 is removeLoops of G1 )

proof end;

theorem :: GLIB_009:126

for G1 being non-Dmulti _Graph

for G2 being _Graph holds

( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

for G2 being _Graph holds

( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

proof end;

registration

let G be _Graph;

coherence

for b_{1} being SimpleGraph of G holds

( b_{1} is spanning & b_{1} is loopless & b_{1} is non-multi & b_{1} is simple )

for b_{1} being DSimpleGraph of G holds

( b_{1} is spanning & b_{1} is loopless & b_{1} is non-Dmulti & b_{1} is Dsimple )

ex b_{1} being SimpleGraph of G st b_{1} is plain

ex b_{1} being DSimpleGraph of G st b_{1} is plain

end;
coherence

for b

( b

proof end;

coherence for b

( b

proof end;

existence ex b

proof end;

existence ex b

proof end;

theorem Th133: :: GLIB_009:133

for G1 being _Graph

for G2 being DSimpleGraph of G1

for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1

for G2 being DSimpleGraph of G1

for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1

proof end;

theorem :: GLIB_009:134

for G1 being _Graph

for G2 being DSimpleGraph of G1 ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2

for G2 being DSimpleGraph of G1 ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2

proof end;

theorem :: GLIB_009:135

for G1 being _Graph

for G3 being SimpleGraph of G1 ex G2 being DSimpleGraph of G1 st G3 is SimpleGraph of G2

for G3 being SimpleGraph of G1 ex G2 being DSimpleGraph of G1 st G3 is SimpleGraph of G2

proof end;

registration

let G be complete _Graph;

coherence

for b_{1} being SimpleGraph of G holds b_{1} is complete

for b_{1} being DSimpleGraph of G holds b_{1} is complete

end;
coherence

for b

proof end;

coherence for b

proof end;

theorem Th136: :: GLIB_009:136

for G1 being _Graph

for G2 being SimpleGraph of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

for G2 being SimpleGraph of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th137: :: GLIB_009:137

for G1 being _Graph

for G2 being DSimpleGraph of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

for G2 being DSimpleGraph of G1

for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th138: :: GLIB_009:138

for G1 being _Graph

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

theorem Th139: :: GLIB_009:139

for G1 being _Graph

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

registration

let G be connected _Graph;

coherence

for b_{1} being SimpleGraph of G holds b_{1} is connected

for b_{1} being DSimpleGraph of G holds b_{1} is connected

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let G be non connected _Graph;

coherence

for b_{1} being SimpleGraph of G holds not b_{1} is connected

for b_{1} being DSimpleGraph of G holds not b_{1} is connected

end;
coherence

for b

proof end;

coherence for b

proof end;

:: non chordal cluster after non chordal has been clustered with cycles

registration

let G be chordal _Graph;

coherence

for b_{1} being SimpleGraph of G holds b_{1} is chordal
by Th144;

coherence

for b_{1} being DSimpleGraph of G holds b_{1} is chordal
by Th145;

end;
coherence

for b

coherence

for b

theorem :: GLIB_009:146

for G1 being _Graph

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem :: GLIB_009:147

for G1 being _Graph

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem :: GLIB_009:148

for G1 being loopless _Graph

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

proof end;

theorem :: GLIB_009:149

for G1 being loopless _Graph

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v1 is isolated iff v2 is isolated )

proof end;

theorem :: GLIB_009:150

for G1 being _Graph

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

for G2 being SimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

proof end;

theorem :: GLIB_009:151

for G1 being _Graph

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

for G2 being DSimpleGraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds

v2 is endvertex

proof end;