:: by Sebastian Koch
::
:: Copyright (c) 2021 Association of Mizar Users

Lm1: for X, Y being set
for f being Function of X,Y
for V being ManySortedSet of Y
for E being one-to-one ManySortedSet of X holds (V * f) * (E ") is Function of (rng E),(rng V)

proof end;

definition
let G be _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
func replaceVerticesEdges (V,E) -> plain _Graph means :Def1: :: GLIB_015:def 1
ex S, T being Function of (rng E),(rng V) st
( S = (V * ()) * (E ") & T = (V * ()) * (E ") & it = createGraph ((rng V),(rng E),S,T) );
existence
ex b1 being plain _Graph ex S, T being Function of (rng E),(rng V) st
( S = (V * ()) * (E ") & T = (V * ()) * (E ") & b1 = createGraph ((rng V),(rng E),S,T) )
proof end;
uniqueness
for b1, b2 being plain _Graph st ex S, T being Function of (rng E),(rng V) st
( S = (V * ()) * (E ") & T = (V * ()) * (E ") & b1 = createGraph ((rng V),(rng E),S,T) ) & ex S, T being Function of (rng E),(rng V) st
( S = (V * ()) * (E ") & T = (V * ()) * (E ") & b2 = createGraph ((rng V),(rng E),S,T) ) holds
b1 = b2
;
end;

:: deftheorem Def1 defines replaceVerticesEdges GLIB_015:def 1 :
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for b4 being plain _Graph holds
( b4 = replaceVerticesEdges (V,E) iff ex S, T being Function of (rng E),(rng V) st
( S = (V * ()) * (E ") & T = (V * ()) * (E ") & b4 = createGraph ((rng V),(rng E),S,T) ) );

definition
let G be _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
func replaceVertices V -> plain _Graph equals :: GLIB_015:def 2
replaceVerticesEdges (V,(id ()));
coherence
replaceVerticesEdges (V,(id ())) is plain _Graph
;
end;

:: deftheorem defines replaceVertices GLIB_015:def 2 :
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G holds replaceVertices V = replaceVerticesEdges (V,(id ()));

definition
let G be _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
func replaceEdges E -> plain _Graph equals :: GLIB_015:def 3
replaceVerticesEdges ((),E);
coherence
replaceVerticesEdges ((),E) is plain _Graph
;
end;

:: deftheorem defines replaceEdges GLIB_015:def 3 :
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G holds replaceEdges E = replaceVerticesEdges ((),E);

theorem Th1: :: GLIB_015:1
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G holds
( the_Vertices_of (replaceVerticesEdges (V,E)) = rng V & the_Edges_of (replaceVerticesEdges (V,E)) = rng E & the_Source_of (replaceVerticesEdges (V,E)) = (V * ()) * (E ") & the_Target_of (replaceVerticesEdges (V,E)) = (V * ()) * (E ") )
proof end;

theorem Th2: :: GLIB_015:2
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G holds
( the_Vertices_of () = rng V & the_Edges_of () = the_Edges_of G & the_Source_of () = V * () & the_Target_of () = V * () )
proof end;

theorem Th3: :: GLIB_015:3
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G holds
( the_Vertices_of () = the_Vertices_of G & the_Edges_of () = rng E & the_Source_of () = () * (E ") & the_Target_of () = () * (E ") )
proof end;

theorem Th4: :: GLIB_015:4
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e DJoins v,w,G holds
E . e DJoins V . v,V . w, replaceVerticesEdges (V,E)
proof end;

theorem Th5: :: GLIB_015:5
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e, v, w being object st e DJoins v,w,G holds
e DJoins V . v,V . w, replaceVertices V
proof end;

theorem Th6: :: GLIB_015:6
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e DJoins v,w,G holds
E . e DJoins v,w, replaceEdges E
proof end;

theorem :: GLIB_015:7
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e Joins v,w,G holds
E . e Joins V . v,V . w, replaceVerticesEdges (V,E)
proof end;

theorem :: GLIB_015:8
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e, v, w being object st e Joins v,w,G holds
e Joins V . v,V . w, replaceVertices V
proof end;

theorem :: GLIB_015:9
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e Joins v,w,G holds
E . e Joins v,w, replaceEdges E
proof end;

theorem Th10: :: GLIB_015:10
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e in dom E & v in dom V & w in dom V & E . e DJoins V . v,V . w, replaceVerticesEdges (V,E) holds
e DJoins v,w,G
proof end;

theorem Th11: :: GLIB_015:11
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e, v, w being object st v in dom V & w in dom V & e DJoins V . v,V . w, replaceVertices V holds
e DJoins v,w,G
proof end;

theorem Th12: :: GLIB_015:12
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e in dom E & E . e DJoins v,w, replaceEdges E holds
e DJoins v,w,G
proof end;

theorem :: GLIB_015:13
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e in dom E & v in dom V & w in dom V & E . e Joins V . v,V . w, replaceVerticesEdges (V,E) holds
e Joins v,w,G
proof end;

theorem :: GLIB_015:14
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e, v, w being object st v in dom V & w in dom V & e Joins V . v,V . w, replaceVertices V holds
e Joins v,w,G
proof end;

theorem :: GLIB_015:15
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e in dom E & E . e Joins v,w, replaceEdges E holds
e Joins v,w,G
proof end;

theorem Th16: :: GLIB_015:16
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G ex F being PGraphMapping of G, replaceVerticesEdges (V,E) st
( F _V = V & F _E = E & F is Disomorphism )
proof end;

theorem Th17: :: GLIB_015:17
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G holds replaceVerticesEdges (V,E) is G -Disomorphic
proof end;

:: clusterings (from Disomorphic)
registration
let G be loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is loopless
proof end;
end;

registration
let G be loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be loopless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non loopless plain ;
coherence
not replaceVerticesEdges (V,E) is loopless
proof end;
end;

registration
let G be non loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is loopless
;
end;

registration
let G be non loopless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is loopless
;
end;

registration
let G be non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is non-multi
proof end;
end;

registration
let G be non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be non-multi _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non non-multi plain ;
coherence
not replaceVerticesEdges (V,E) is non-multi
proof end;
end;

registration
let G be non non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is non-multi
;
end;

registration
let G be non non-multi _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is non-multi
;
end;

registration
let G be non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is non-Dmulti
proof end;
end;

registration
let G be non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be non-Dmulti _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non non-Dmulti plain ;
coherence
not replaceVerticesEdges (V,E) is non-Dmulti
proof end;
end;

registration
let G be non non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be non non-Dmulti _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is non-Dmulti
;
end;

registration
let G be simple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is simple
;
end;

registration
let G be simple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be simple _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be Dsimple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is Dsimple
;
end;

registration
let G be Dsimple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be Dsimple _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is _trivial
proof end;
end;

registration
let G be _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be _trivial _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non _trivial plain ;
coherence
not replaceVerticesEdges (V,E) is _trivial
proof end;
end;

registration
let G be non _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is _trivial
;
end;

registration
let G be non _trivial _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is _trivial
;
end;

registration
let G be vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
proof end;
end;

registration
let G be vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be vertex-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceVerticesEdges (V,E) is vertex-finite
proof end;
end;

registration
let G be non vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be non vertex-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is edge-finite
proof end;
end;

registration
let G be edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be edge-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> plain non edge-finite ;
coherence
not replaceVerticesEdges (V,E) is edge-finite
proof end;
end;

registration
let G be non edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be non edge-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is edge-finite
;
end;

registration
let G be _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> plain ;
coherence
replaceVerticesEdges (V,E) is finite
;
end;

registration
let G be _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is acyclic
proof end;
end;

registration
let G be acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be acyclic _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non acyclic plain ;
coherence
not replaceVerticesEdges (V,E) is acyclic
proof end;
end;

registration
let G be non acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is acyclic
;
end;

registration
let G be non acyclic _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is acyclic
;
end;

registration
let G be connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is connected
proof end;
end;

registration
let G be connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be connected _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non connected plain ;
coherence
not replaceVerticesEdges (V,E) is connected
proof end;
end;

registration
let G be non connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is connected
;
end;

registration
let G be non connected _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is connected
;
end;

registration
let G be Tree-like _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is Tree-like
;
end;

registration
let G be Tree-like _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be Tree-like _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be chordal _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is chordal
proof end;
end;

registration
let G be chordal _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be chordal _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

:: clustering for non chordal graphs will be done after existence clustering
:: registration
:: let G be non chordal _Graph;
:: let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
:: let E be one-to-one ManySortedSet of the_Edges_of G;
:: cluster replaceVerticesEdges(V,E) -> non chordal;
:: coherence;
:: end;
::
:: registration
:: let G be non chordal _Graph;
:: let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
:: cluster replaceVertices(V) -> non chordal;
:: coherence;
:: end;
::
:: registration
:: let G be non chordal _Graph;
:: let E be one-to-one ManySortedSet of the_Edges_of G;
:: cluster replaceEdges(E) -> non chordal;
:: coherence;
:: end;
registration
let G be edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is edgeless
proof end;
end;

registration
let G be edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be edgeless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> non edgeless plain ;
coherence
not replaceVerticesEdges (V,E) is edgeless
proof end;
end;

registration
let G be non edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is edgeless
;
end;

registration
let G be non edgeless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is edgeless
;
end;

registration
let G be loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is loopfull
proof end;
end;

registration
let G be loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be loopfull _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges (V,E) -> plain non loopfull ;
coherence
not replaceVerticesEdges (V,E) is loopfull
proof end;
end;

registration
let G be non loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence
not replaceVertices V is loopfull
;
end;

registration
let G be non loopfull _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceEdges E is loopfull
;
end;

registration
let G be locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
proof end;
end;

registration
let G be locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be locally-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let G be non locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
not replaceVerticesEdges (V,E) is locally-finite
proof end;
end;

registration
let G be non locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let G be non locally-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let c be non zero Cardinal;
let G be c -vertex _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is c -vertex
proof end;
end;

registration
let c be non zero Cardinal;
let G be c -vertex _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let c be non zero Cardinal;
let G be c -vertex _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

registration
let c be Cardinal;
let G be c -edge _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence
replaceVerticesEdges (V,E) is c -edge
proof end;
end;

registration
let c be Cardinal;
let G be c -edge _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
coherence ;
end;

registration
let c be Cardinal;
let G be c -edge _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
coherence ;
end;

theorem Th18: :: GLIB_015:18
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for W1 being Walk of G ex W2 being Walk of replaceVerticesEdges (V,E) st
( V * () = W2 .vertexSeq() & E * () = W2 .edgeSeq() )
proof end;

theorem :: GLIB_015:19
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for W1 being Walk of G ex W2 being Walk of replaceVertices V st
( V * () = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() )
proof end;

theorem :: GLIB_015:20
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for W1 being Walk of G ex W2 being Walk of replaceEdges E st
( W1 .vertexSeq() = W2 .vertexSeq() & E * () = W2 .edgeSeq() )
proof end;

theorem Th21: :: GLIB_015:21
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for W2 being Walk of replaceVerticesEdges (V,E) ex W1 being Walk of G st
( V * () = W2 .vertexSeq() & E * () = W2 .edgeSeq() )
proof end;

theorem :: GLIB_015:22
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for W2 being Walk of replaceVertices V ex W1 being Walk of G st
( V * () = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() )
proof end;

theorem :: GLIB_015:23
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
for W2 being Walk of replaceEdges E ex W1 being Walk of G st
( W1 .vertexSeq() = W2 .vertexSeq() & E * () = W2 .edgeSeq() )
proof end;

definition
let F be Graph-yielding Function;
func the_Vertices_of F -> Function means :Def4: :: GLIB_015:def 4
( dom it = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & it . x = the_Vertices_of G ) ) );
existence
ex b1 being Function st
( dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Vertices_of G ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Vertices_of G ) ) & dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Vertices_of G ) ) holds
b1 = b2
proof end;
func the_Edges_of F -> Function means :Def5: :: GLIB_015:def 5
( dom it = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & it . x = the_Edges_of G ) ) );
existence
ex b1 being Function st
( dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Edges_of G ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Edges_of G ) ) & dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Edges_of G ) ) holds
b1 = b2
proof end;
func the_Source_of F -> Function means :Def6: :: GLIB_015:def 6
( dom it = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & it . x = the_Source_of G ) ) );
existence
ex b1 being Function st
( dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Source_of G ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Source_of G ) ) & dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Source_of G ) ) holds
b1 = b2
proof end;
func the_Target_of F -> Function means :Def7: :: GLIB_015:def 7
( dom it = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & it . x = the_Target_of G ) ) );
existence
ex b1 being Function st
( dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Target_of G ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b1 . x = the_Target_of G ) ) & dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Target_of G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines the_Vertices_of GLIB_015:def 4 :
for F being Graph-yielding Function
for b2 being Function holds
( b2 = the_Vertices_of F iff ( dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Vertices_of G ) ) ) );

:: deftheorem Def5 defines the_Edges_of GLIB_015:def 5 :
for F being Graph-yielding Function
for b2 being Function holds
( b2 = the_Edges_of F iff ( dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Edges_of G ) ) ) );

:: deftheorem Def6 defines the_Source_of GLIB_015:def 6 :
for F being Graph-yielding Function
for b2 being Function holds
( b2 = the_Source_of F iff ( dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Source_of G ) ) ) );

:: deftheorem Def7 defines the_Target_of GLIB_015:def 7 :
for F being Graph-yielding Function
for b2 being Function holds
( b2 = the_Target_of F iff ( dom b2 = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & b2 . x = the_Target_of G ) ) ) );

registration
let F be Graph-yielding Function;
coherence
proof end;
coherence
proof end;
end;

registration
let F be empty Graph-yielding Function;
coherence
proof end;
coherence
proof end;
coherence
proof end;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding Function;
cluster the_Vertices_of F -> non empty ;
coherence
not the_Vertices_of F is empty
proof end;
cluster the_Edges_of F -> non empty ;
coherence
not the_Edges_of F is empty
proof end;
cluster the_Source_of F -> non empty ;
coherence
not the_Source_of F is empty
proof end;
cluster the_Target_of F -> non empty ;
coherence
not the_Target_of F is empty
proof end;
end;

registration
let F be Graph-yielding Function;
coherence
proof end;
end;

definition
let F be non empty Graph-yielding Function;
redefine func the_Vertices_of F means :Def8: :: GLIB_015:def 8
( dom it = dom F & ( for x being Element of dom F holds it . x = the_Vertices_of (F . x) ) );
compatibility
for b1 being Function holds
( b1 = the_Vertices_of F iff ( dom b1 = dom F & ( for x being Element of dom F holds b1 . x = the_Vertices_of (F . x) ) ) )
proof end;
redefine func the_Edges_of F means :Def9: :: GLIB_015:def 9
( dom it = dom F & ( for x being Element of dom F holds it . x = the_Edges_of (F . x) ) );
compatibility
for b1 being Function holds
( b1 = the_Edges_of F iff ( dom b1 = dom F & ( for x being Element of dom F holds b1 . x = the_Edges_of (F . x) ) ) )
proof end;
redefine func the_Source_of F means :: GLIB_015:def 10
( dom it = dom F & ( for x being Element of dom F holds it . x = the_Source_of (F . x) ) );
compatibility
for b1 being Function holds
( b1 = the_Source_of F iff ( dom b1 = dom F & ( for x being Element of dom F holds b1 . x = the_Source_of (F . x) ) ) )
proof end;
redefine func the_Target_of F means :: GLIB_015:def 11
( dom it = dom F & ( for x being Element of dom F holds it . x = the_Target_of (F . x) ) );
compatibility
for b1 being Function holds
( b1 = the_Target_of F iff ( dom b1 = dom F & ( for x being Element of dom F holds b1 . x = the_Target_of (F . x) ) ) )
proof end;
end;

:: deftheorem Def8 defines the_Vertices_of GLIB_015:def 8 :
for F being non empty Graph-yielding Function
for b2 being Function holds
( b2 = the_Vertices_of F iff ( dom b2 = dom F & ( for x being Element of dom F holds b2 . x = the_Vertices_of (F . x) ) ) );

:: deftheorem Def9 defines the_Edges_of GLIB_015:def 9 :
for F being non empty Graph-yielding Function
for b2 being Function holds
( b2 = the_Edges_of F iff ( dom b2 = dom F & ( for x being Element of dom F holds b2 . x = the_Edges_of (F . x) ) ) );

:: deftheorem defines the_Source_of GLIB_015:def 10 :
for F being non empty Graph-yielding Function
for b2 being Function holds
( b2 = the_Source_of F iff ( dom b2 = dom F & ( for x being Element of dom F holds b2 . x = the_Source_of (F . x) ) ) );

:: deftheorem defines the_Target_of GLIB_015:def 11 :
for F being non empty Graph-yielding Function
for b2 being Function holds
( b2 = the_Target_of F iff ( dom b2 = dom F & ( for x being Element of dom F holds b2 . x = the_Target_of (F . x) ) ) );

theorem :: GLIB_015:24
for F being Graph-yielding Function holds the_Vertices_of (rng F) = rng ()
proof end;

theorem :: GLIB_015:25
for F being Graph-yielding Function holds the_Edges_of (rng F) = rng ()
proof end;

theorem :: GLIB_015:26
for F being Graph-yielding Function holds the_Source_of (rng F) = rng ()
proof end;

theorem :: GLIB_015:27
for F being Graph-yielding Function holds the_Target_of (rng F) = rng ()
proof end;

definition
let S1, S2 be Graph-membered set ;
pred S1,S2 are_Disomorphic means :: GLIB_015:def 12
ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b2 -Disomorphic _Graph ) );
reflexivity
for S1 being Graph-membered set ex f being one-to-one Function st
( dom f = S1 & rng f = S1 & ( for G being _Graph st G in S1 holds
f . G is b3 -Disomorphic _Graph ) )
proof end;
symmetry
for S1, S2 being Graph-membered set st ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b4 -Disomorphic _Graph ) ) holds
ex f being one-to-one Function st
( dom f = S2 & rng f = S1 & ( for G being _Graph st G in S2 holds
f . G is b4 -Disomorphic _Graph ) )
proof end;
pred S1,S2 are_isomorphic means :: GLIB_015:def 13
ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b2 -isomorphic _Graph ) );
reflexivity
for S1 being Graph-membered set ex f being one-to-one Function st
( dom f = S1 & rng f = S1 & ( for G being _Graph st G in S1 holds
f . G is b3 -isomorphic _Graph ) )
proof end;
symmetry
for S1, S2 being Graph-membered set st ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b4 -isomorphic _Graph ) ) holds
ex f being one-to-one Function st
( dom f = S2 & rng f = S1 & ( for G being _Graph st G in S2 holds
f . G is b4 -isomorphic _Graph ) )
proof end;
end;

:: deftheorem defines are_Disomorphic GLIB_015:def 12 :
for S1, S2 being Graph-membered set holds
( S1,S2 are_Disomorphic iff ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b4 -Disomorphic _Graph ) ) );

:: deftheorem defines are_isomorphic GLIB_015:def 13 :
for S1, S2 being Graph-membered set holds
( S1,S2 are_isomorphic iff ex f being one-to-one Function st
( dom f = S1 & rng f = S2 & ( for G being _Graph st G in S1 holds
f . G is b4 -isomorphic _Graph ) ) );

theorem :: GLIB_015:28
for S1, S2, S3 being Graph-membered set st S1,S2 are_Disomorphic & S2,S3 are_Disomorphic holds
S1,S3 are_Disomorphic
proof end;

theorem :: GLIB_015:29
for S1, S2, S3 being Graph-membered set st S1,S2 are_isomorphic & S2,S3 are_isomorphic holds
S1,S3 are_isomorphic
proof end;

theorem :: GLIB_015:30
for S1, S2 being Graph-membered set st S1,S2 are_Disomorphic holds
S1,S2 are_isomorphic
proof end;

theorem :: GLIB_015:31
for S1, S2 being Graph-membered set st S1,S2 are_Disomorphic holds
card S1 = card S2 by CARD_1:70;

theorem :: GLIB_015:32
for S1, S2 being Graph-membered set st S1,S2 are_isomorphic holds
card S1 = card S2 by CARD_1:70;

theorem :: GLIB_015:33
for S1, S2 being empty Graph-membered set holds S1,S2 are_Disomorphic ;

theorem :: GLIB_015:34
for G1, G2 being _Graph holds
( {G1},{G2} are_Disomorphic iff G2 is G1 -Disomorphic )
proof end;

theorem :: GLIB_015:35
for G1, G2 being _Graph holds
( {G1},{G2} are_isomorphic iff G2 is G1 -isomorphic )
proof end;

theorem :: GLIB_015:36
for S1, S2 being Graph-membered set st S1,S2 are_isomorphic holds
( ( S1 is empty implies S2 is empty ) & ( S1 is loopless implies S2 is loopless ) & ( S1 is non-multi implies S2 is non-multi ) & ( S1 is simple implies S2 is simple ) & ( S1 is acyclic implies S2 is acyclic ) & ( S1 is connected implies S2 is connected ) & ( S1 is Tree-like implies S2 is Tree-like ) & ( S1 is chordal implies S2 is chordal ) & ( S1 is edgeless implies S2 is edgeless ) & ( S1 is loopfull implies S2 is loopfull ) )
proof end;

theorem :: GLIB_015:37
for S1, S2 being Graph-membered set st S1,S2 are_Disomorphic holds
( ( S1 is non-Dmulti implies S2 is non-Dmulti ) & ( S1 is Dsimple implies S2 is Dsimple ) )
proof end;

definition
let F1, F2 be Graph-yielding Function;
pred F1,F2 are_Disomorphic means :: GLIB_015:def 14
ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) ) );
reflexivity
for F1 being Graph-yielding Function ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F1 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F1 . (p . x) & G2 is G1 -Disomorphic ) ) )
proof end;
symmetry
for F1, F2 being Graph-yielding Function st ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) ) ) holds
ex p being one-to-one Function st
( dom p = dom F2 & rng p = dom F1 & ( for x being object st x in dom F2 holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -Disomorphic ) ) )
proof end;
pred F1,F2 are_isomorphic means :: GLIB_015:def 15
ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) ) );
reflexivity
for F1 being Graph-yielding Function ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F1 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic ) ) )
proof end;
symmetry
for F1, F2 being Graph-yielding Function st ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) ) ) holds
ex p being one-to-one Function st
( dom p = dom F2 & rng p = dom F1 & ( for x being object st x in dom F2 holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic ) ) )
proof end;
end;

:: deftheorem defines are_Disomorphic GLIB_015:def 14 :
for F1, F2 being Graph-yielding Function holds
( F1,F2 are_Disomorphic iff ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) ) ) );

:: deftheorem defines are_isomorphic GLIB_015:def 15 :
for F1, F2 being Graph-yielding Function holds
( F1,F2 are_isomorphic iff ex p being one-to-one Function st
( dom p = dom F1 & rng p = dom F2 & ( for x being object st x in dom F1 holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) ) ) );

theorem Th38: :: GLIB_015:38
for F1, F2 being non empty Graph-yielding Function st dom F1 = dom F2 & ( for x1 being Element of dom F1
for x2 being Element of dom F2 st x1 = x2 holds
F2 . x2 is F1 . x1 -Disomorphic ) holds
F1,F2 are_Disomorphic
proof end;

theorem :: GLIB_015:39
for F1, F2 being non empty Graph-yielding Function st dom F1 = dom F2 & ( for x1 being Element of dom F1
for x2 being Element of dom F2 st x1 = x2 holds
F2 . x2 is F1 . x1 -isomorphic ) holds
F1,F2 are_isomorphic
proof end;

theorem Th40: :: GLIB_015:40
for F1, F2, F3 being Graph-yielding Function st F1,F2 are_Disomorphic & F2,F3 are_Disomorphic holds
F1,F3 are_Disomorphic
proof end;

theorem Th41: :: GLIB_015:41
for F1, F2, F3 being Graph-yielding Function st F1,F2 are_isomorphic & F2,F3 are_isomorphic holds
F1,F3 are_isomorphic
proof end;

theorem Th42: :: GLIB_015:42
for F1, F2 being Graph-yielding Function st F1,F2 are_Disomorphic holds
F1,F2 are_isomorphic
proof end;

theorem :: GLIB_015:43
for F1, F2 being empty Graph-yielding Function holds
( F1,F2 are_Disomorphic & F1,F2 are_isomorphic ) ;

theorem :: GLIB_015:44
for F1, F2 being Graph-yielding Function st F1,F2 are_Disomorphic holds
card F1 = card F2
proof end;

theorem :: GLIB_015:45
for F1, F2 being Graph-yielding Function st F1,F2 are_isomorphic holds
card F1 = card F2
proof end;

theorem :: GLIB_015:46
for G1, G2 being _Graph
for x, y being object holds
( x .--> G1,y .--> G2 are_Disomorphic iff G2 is G1 -Disomorphic )
proof end;

theorem :: GLIB_015:47
for G1, G2 being _Graph
for x, y being object holds
( x .--> G1,y .--> G2 are_isomorphic iff G2 is G1 -isomorphic )
proof end;

theorem Th48: :: GLIB_015:48
for F1, F2 being Graph-yielding Function st F1,F2 are_isomorphic holds
( ( F1 is empty implies F2 is empty ) & ( F1 is loopless implies F2 is loopless ) & ( F1 is non-multi implies F2 is non-multi ) & ( F1 is simple implies F2 is simple ) & ( F1 is acyclic implies F2 is acyclic ) & ( F1 is connected implies F2 is connected ) & ( F1 is Tree-like implies F2 is Tree-like ) & ( F1 is chordal implies F2 is chordal ) & ( F1 is edgeless implies F2 is edgeless ) & ( F1 is loopfull implies F2 is loopfull ) )
proof end;

theorem Th49: :: GLIB_015:49
for F1, F2 being Graph-yielding Function st F1,F2 are_Disomorphic holds
( ( F1 is non-Dmulti implies F2 is non-Dmulti ) & ( F1 is Dsimple implies F2 is Dsimple ) )
proof end;

definition
let I be set ;
let F1, F2 be Graph-yielding ManySortedSet of I;
:: original: are_Disomorphic
redefine pred F1,F2 are_Disomorphic means :: GLIB_015:def 16
ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic );
compatibility
( F1,F2 are_Disomorphic iff ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) )
proof end;
reflexivity
for F1 being Graph-yielding ManySortedSet of I ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F1 . (p . x) & G2 is G1 -Disomorphic )
proof end;
symmetry
for F1, F2 being Graph-yielding ManySortedSet of I st ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) holds
ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -Disomorphic )
proof end;
:: original: are_isomorphic
redefine pred F1,F2 are_isomorphic means :: GLIB_015:def 17
ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic );
compatibility
( F1,F2 are_isomorphic iff ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) )
proof end;
reflexivity
for F1 being Graph-yielding ManySortedSet of I ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic )
proof end;
symmetry
for F1, F2 being Graph-yielding ManySortedSet of I st ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) holds
ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F2 . x & G2 = F1 . (p . x) & G2 is G1 -isomorphic )
proof end;
end;

:: deftheorem defines are_Disomorphic GLIB_015:def 16 :
for I being set
for F1, F2 being Graph-yielding ManySortedSet of I holds
( F1,F2 are_Disomorphic iff ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -Disomorphic ) );

:: deftheorem defines are_isomorphic GLIB_015:def 17 :
for I being set
for F1, F2 being Graph-yielding ManySortedSet of I holds
( F1,F2 are_isomorphic iff ex p being Permutation of I st
for x being object st x in I holds
ex G1, G2 being _Graph st
( G1 = F1 . x & G2 = F2 . (p . x) & G2 is G1 -isomorphic ) );

definition
let S be Graph-membered set ;
attr S is vertex-disjoint means :Def18: :: GLIB_015:def 18
for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
the_Vertices_of G1 misses the_Vertices_of G2;
attr S is edge-disjoint means :Def19: :: GLIB_015:def 19
for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
the_Edges_of G1 misses the_Edges_of G2;
end;

:: deftheorem Def18 defines vertex-disjoint GLIB_015:def 18 :
for S being Graph-membered set holds
( S is vertex-disjoint iff for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
the_Vertices_of G1 misses the_Vertices_of G2 );

:: deftheorem Def19 defines edge-disjoint GLIB_015:def 19 :
for S being Graph-membered set holds
( S is edge-disjoint iff for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
the_Edges_of G1 misses the_Edges_of G2 );

theorem :: GLIB_015:50
for S being Graph-membered set holds
( ( S is vertex-disjoint & S is edge-disjoint ) iff for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds
( the_Vertices_of G1 misses the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 ) ) ;

registration
coherence
for b1 being Graph-membered set st b1 is trivial holds
( b1 is vertex-disjoint & b1 is edge-disjoint )
by ZFMISC_1:def 10;
coherence
for b1 being Graph-membered set st b1 is edgeless holds
b1 is edge-disjoint
proof end;
coherence
for b1 being Graph-membered set st b1 is edge-disjoint holds
b1 is \/-tolerating
proof end;
coherence
for b1 being Graph-membered set st b1 is vertex-disjoint & b1 is \/-tolerating holds
b1 is edge-disjoint
proof end;
end;

registration
let G be _Graph;
coherence
( {G} is vertex-disjoint & {G} is edge-disjoint )
;
end;

theorem :: GLIB_015:51
for G1, G2 being _Graph holds
( {G1,G2} is vertex-disjoint iff ( G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2 ) )
proof end;

theorem :: GLIB_015:52
for G1, G2 being _Graph holds
( {G1,G2} is edge-disjoint iff ( G1 = G2 or the_Edges_of G1 misses the_Edges_of G2 ) )
proof end;

registration
existence
ex b1 being Graph-membered set st
( not b1 is empty & b1 is \/-tolerating & b1 is vertex-disjoint & b1 is edge-disjoint & b1 is acyclic & b1 is simple & b1 is Dsimple & b1 is loopless & b1 is non-multi & b1 is non-Dmulti )
proof end;
end;

:: note that the other direction does not work,
:: for example take S = {G,H} with G == H <> G
registration
let S be Graph-membered vertex-disjoint set ;
coherence
proof end;
end;

registration
let S be Graph-membered edge-disjoint set ;
coherence
proof end;
end;

registration
let S be Graph-membered vertex-disjoint set ;
cluster -> vertex-disjoint for Element of bool S;
coherence
for b1 being Subset of S holds b1 is vertex-disjoint
by Def18;
end;

registration
let S1 be Graph-membered vertex-disjoint set ;
let S2 be set ;
cluster S1 /\ S2 -> vertex-disjoint ;
coherence
S1 /\ S2 is vertex-disjoint
proof end;
cluster S1 \ S2 -> vertex-disjoint ;
coherence
S1 \ S2 is vertex-disjoint
;
end;

registration
let S be Graph-membered edge-disjoint set ;
cluster -> edge-disjoint for Element of bool S;
coherence
for b1 being Subset of S holds b1 is edge-disjoint
by Def19;
end;

registration
let S1 be Graph-membered edge-disjoint set ;
let S2 be set ;
cluster S1 /\ S2 -> edge-disjoint ;
coherence
S1 /\ S2 is edge-disjoint
proof end;
cluster S1 \ S2 -> edge-disjoint ;
coherence
S1 \ S2 is edge-disjoint
;
end;

theorem :: GLIB_015:53
for S1, S2 being Graph-membered set st S1 \/ S2 is vertex-disjoint holds
( S1 is vertex-disjoint & S2 is vertex-disjoint )
proof end;

theorem :: GLIB_015:54
for S1, S2 being Graph-membered set st S1 \/ S2 is edge-disjoint holds
( S1 is edge-disjoint & S2 is edge-disjoint )
proof end;

theorem Th55: :: GLIB_015:55
for S1, S2 being vertex-disjoint GraphUnionSet
for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st S1,S2 are_Disomorphic holds
G2 is G1 -Disomorphic
proof end;

theorem Th56: :: GLIB_015:56
for S1, S2 being vertex-disjoint GraphUnionSet
for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st S1,S2 are_isomorphic holds
ex S3 being vertex-disjoint GraphUnionSet ex E being Subset of () ex G3 being GraphUnion of S3 st
( S1,S3 are_Disomorphic & G3 is reverseEdgeDirections of G2,E )
proof end;

theorem Th57: :: GLIB_015:57
for S1, S2 being vertex-disjoint GraphUnionSet
for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st S1,S2 are_isomorphic holds
G2 is G1 -isomorphic
proof end;

theorem Th58: :: GLIB_015:58
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S
for W being Walk of G ex H being Element of S st W is Walk of H
proof end;

theorem Th59: :: GLIB_015:59
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S st G is connected holds
ex H being _Graph st S = {H}
proof end;

theorem Th60: :: GLIB_015:60
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S holds
( ( S is non-multi implies G is non-multi ) & ( G is non-multi implies S is non-multi ) & ( S is non-Dmulti implies G is non-Dmulti ) & ( G is non-Dmulti implies S is non-Dmulti ) & ( S is acyclic implies G is acyclic ) & ( G is acyclic implies S is acyclic ) )
proof end;

theorem :: GLIB_015:61
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S holds
( ( S is simple implies G is simple ) & ( G is simple implies S is simple ) & ( S is Dsimple implies G is Dsimple ) & ( G is Dsimple implies S is Dsimple ) )
proof end;

registration
let S be non-multi vertex-disjoint GraphUnionSet;
cluster -> non-multi for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is non-multi
by Th60;
end;

registration
let S be non-Dmulti vertex-disjoint GraphUnionSet;
cluster -> non-Dmulti for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is non-Dmulti
by Th60;
end;

registration
let S be simple vertex-disjoint GraphUnionSet;
cluster -> simple for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is simple
;
end;

registration
let S be Dsimple vertex-disjoint GraphUnionSet;
cluster -> Dsimple for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is Dsimple
;
end;

registration
let S be acyclic vertex-disjoint GraphUnionSet;
cluster -> acyclic for GraphUnion of S;
coherence
for b1 being GraphUnion of S holds b1 is acyclic
by Th60;
end;

theorem Th62: :: GLIB_015:62
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S
for H being Element of S holds H is inducedSubgraph of G,()
proof end;

theorem Th63: :: GLIB_015:63
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S holds
( ( S is chordal implies G is chordal ) & ( G is chordal implies S is chordal ) & ( S is loopfull implies G is loopfull ) & ( G is loopfull implies S is loopfull ) )
proof end;

theorem Th64: :: GLIB_015:64
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S
for H being Element of S
for v being Vertex of G
for w being Vertex of H st v = w holds
G .reachableFrom v = H .reachableFrom w
proof end;

theorem Th65: :: GLIB_015:65
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S holds G .componentSet() = union { () where H is Element of S : verum }
proof end;

theorem Th66: :: GLIB_015:66
for S being non empty Graph-membered vertex-disjoint set holds { () where H is Element of S : verum } is mutually-disjoint
proof end;

Lm2: for S being non empty Graph-membered vertex-disjoint set holds card S = card { () where H is Element of S : verum }
proof end;

theorem Th67: :: GLIB_015:67
for S being non empty Graph-membered connected set holds { () where H is Element of S : verum } = SmallestPartition ()
proof end;

Lm3: for X being non empty set holds 1 c= card X
proof end;

theorem Th68: :: GLIB_015:68
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S holds card S c= G .numComponents()
proof end;

theorem Th69: :: GLIB_015:69
for S being vertex-disjoint GraphUnionSet
for G being GraphUnion of S st S is connected holds
card S = G .numComponents()
proof end;

definition
let F be Graph-yielding Function;
attr F is vertex-disjoint means :Def20: :: GLIB_015:def 20
for x1, x2 being object st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Vertices_of G1 misses the_Vertices_of G2 );
attr F is edge-disjoint means :Def21: :: GLIB_015:def 21
for x1, x2 being object st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Edges_of G1 misses the_Edges_of G2 );
end;

:: deftheorem Def20 defines vertex-disjoint GLIB_015:def 20 :
for F being Graph-yielding Function holds
( F is vertex-disjoint iff for x1, x2 being object st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Vertices_of G1 misses the_Vertices_of G2 ) );

:: deftheorem Def21 defines edge-disjoint GLIB_015:def 21 :
for F being Graph-yielding Function holds
( F is edge-disjoint iff for x1, x2 being object st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex G1, G2 being _Graph st
( G1 = F . x1 & G2 = F . x2 & the_Edges_of G1 misses the_Edges_of G2 ) );

:: note that edge-disjoint -> one-to-one doesn't hold because of edgeless graphs
registration
coherence
for b1 being Graph-yielding Function st b1 is trivial holds
( b1 is vertex-disjoint & b1 is edge-disjoint )
by ZFMISC_1:def 10;
coherence
for b1 being Graph-yielding Function st b1 is vertex-disjoint holds
b1 is one-to-one
proof end;
end;

definition
let F be non empty Graph-yielding Function;
redefine attr F is vertex-disjoint means :Def22: :: GLIB_015:def 22
for x1, x2 being Element of dom F st x1 <> x2 holds
the_Vertices_of (F . x1) misses the_Vertices_of (F . x2);
compatibility
( F is vertex-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
the_Vertices_of (F . x1) misses the_Vertices_of (F . x2) )
proof end;
redefine attr F is edge-disjoint means :Def23: :: GLIB_015:def 23
for x1, x2 being Element of dom F st x1 <> x2 holds
the_Edges_of (F . x1) misses the_Edges_of (F . x2);
compatibility
( F is edge-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
the_Edges_of (F . x1) misses the_Edges_of (F . x2) )
proof end;
end;

:: deftheorem Def22 defines vertex-disjoint GLIB_015:def 22 :
for F being non empty Graph-yielding Function holds
( F is vertex-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
the_Vertices_of (F . x1) misses the_Vertices_of (F . x2) );

:: deftheorem Def23 defines edge-disjoint GLIB_015:def 23 :
for F being non empty Graph-yielding Function holds
( F is edge-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
the_Edges_of (F . x1) misses the_Edges_of (F . x2) );

theorem Th70: :: GLIB_015:70
for F being non empty Graph-yielding Function holds
( F is vertex-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
() . x1 misses () . x2 )
proof end;

theorem Th71: :: GLIB_015:71
for F being non empty Graph-yielding Function holds
( F is edge-disjoint iff for x1, x2 being Element of dom F st x1 <> x2 holds
() . x1 misses () . x2 )
proof end;

theorem :: GLIB_015:72
for F being non empty Graph-yielding Function holds
( ( F is vertex-disjoint & F is edge-disjoint ) iff for x1, x2 being Element of dom F st x1 <> x2 holds
( the_Vertices_of (F . x1) misses the_Vertices_of (F . x2) & the_Edges_of (F . x1) misses the_Edges_of (F . x2) ) ) ;

theorem Th73: :: GLIB_015:73
for F being non empty Graph-yielding Function holds
( ( F is vertex-disjoint & F is edge-disjoint ) iff for x1, x2 being Element of dom F st x1 <> x2 holds
( () . x1 misses () . x2 & () . x1 misses () . x2 ) )
proof end;

registration
let x be object ;
let G be _Graph;
coherence
( x .--> G is vertex-disjoint & x .--> G is edge-disjoint )
proof end;
end;

registration
let G be _Graph;
coherence
( <*G*> is vertex-disjoint & <*G*> is edge-disjoint )
;
end;

registration
existence
ex b1 being Graph-yielding Function st
( not b1 is empty & b1 is vertex-disjoint & b1 is edge-disjoint )
proof end;
end;

registration
let F be Graph-yielding vertex-disjoint Function;
coherence
proof end;
end;

registration
let F be Graph-yielding edge-disjoint Function;
coherence
proof end;
end;

theorem Th74: :: GLIB_015:74
for F1, F2 being non empty one-to-one Graph-yielding Function st F1,F2 are_Disomorphic holds
rng F1, rng F2 are_Disomorphic
proof end;

theorem Th75: :: GLIB_015:75
for F1, F2 being non empty one-to-one Graph-yielding Function st F1,F2 are_isomorphic holds
rng F1, rng F2 are_isomorphic
proof end;

theorem :: GLIB_015:76
for G1, G2 being _Graph holds
( <*G1,G2*> is vertex-disjoint iff the_Vertices_of G1 misses the_Vertices_of G2 )
proof end;

theorem :: GLIB_015:77
for G1, G2 being _Graph holds
( <*G1,G2*> is edge-disjoint iff the_Edges_of G1 misses the_Edges_of G2 )
proof end;

definition
let f be Function;
let x be object ;
func renameElementsDistinctlyFunc (f,x) -> ManySortedSet of f . x equals :: GLIB_015:def 24
<:((f . x) --> [f,x]),(id (f . x)):>;
coherence
<:((f . x) --> [f,x]),(id (f . x)):> is ManySortedSet of f . x
proof end;
end;

:: deftheorem defines renameElementsDistinctlyFunc GLIB_015:def 24 :
for f being Function
for x being object holds renameElementsDistinctlyFunc (f,x) = <:((f . x) --> [f,x]),(id (f . x)):>;

theorem Th78: :: GLIB_015:78
for f being Function
for x, y being object st x in dom f & y in f . x holds
() . y = [f,x,y]
proof end;

theorem Th79: :: GLIB_015:79
for f being Function
for x, z being object st x in dom f & z in rng () holds
ex y being object st
( y in f . x & z = [f,x,y] )
proof end;

theorem Th80: :: GLIB_015:80
for f being Function
for x being object holds rng () = [:{[f,x]},(f . x):]
proof end;

theorem :: GLIB_015:81
for f being Function
for x1, x2 being object holds rng () misses f . x2
proof end;

theorem Th82: :: GLIB_015:82
for f being Function
for x1, x2 being object st x1 <> x2 holds
rng () misses rng ()
proof end;

registration
let f be Function;
let x be object ;
coherence ;
end;

registration
let f be empty Function;
let x be object ;
coherence ;
end;

registration
let f be non empty non-empty Function;
let x be Element of dom f;
cluster renameElementsDistinctlyFunc (f,x) -> non empty ;
coherence
not renameElementsDistinctlyFunc (f,x) is empty
proof end;
end;

registration
let F be non empty Graph-yielding Function;
let x be Element of dom F;
cluster renameElementsDistinctlyFunc ((),x) -> non empty the_Vertices_of (F . x) -defined ;
coherence
( not renameElementsDistinctlyFunc ((),x) is empty & renameElementsDistinctlyFunc ((),x) is the_Vertices_of (F . x) -defined )
proof end;
cluster renameElementsDistinctlyFunc ((),x) -> the_Edges_of (F . x) -defined ;
coherence
renameElementsDistinctlyFunc ((),x) is the_Edges_of (F . x) -defined
proof end;
end;

registration
let F be non empty Graph-yielding Function;
let x be Element of dom F;
coherence
for b1 being the_Vertices_of (F . x) -defined Function st b1 = renameElementsDistinctlyFunc ((),x) holds
b1 is total
proof end;
cluster renameElementsDistinctlyFunc ((),x) -> the_Edges_of (F . x) -defined total for the_Edges_of (F . x) -defined Function;
coherence
for b1 being the_Edges_of (F . x) -defined Function st b1 = renameElementsDistinctlyFunc ((),x) holds
b1 is total
proof end;
end;

definition
let F be non empty Graph-yielding Function;
:: canonical distinction of the graph yielding function
func canGFDistinction F -> Graph-yielding Function means :Def25: :: GLIB_015:def 25
( dom it = dom F & ( for x being Element of dom F holds it . x = replaceVerticesEdges ((),()) ) );
existence
ex b1 being Graph-yielding Function st
( dom b1 = dom F & ( for x being Element of dom F holds b1 . x = replaceVerticesEdges ((),()) ) )
proof end;
uniqueness
for b1, b2 being Graph-yielding Function st dom b1 = dom F & ( for x being Element of dom F holds b1 . x = replaceVerticesEdges ((),()) ) & dom b2 = dom F & ( for x being Element of dom F holds b2 . x = replaceVerticesEdges ((),()) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines canGFDistinction GLIB_015:def 25 :
for F being non empty Graph-yielding Function
for b2 being Graph-yielding Function holds
( b2 = canGFDistinction F iff ( dom b2 = dom F & ( for x being Element of dom F holds b2 . x = replaceVerticesEdges ((),()) ) ) );

registration
let F be non empty Graph-yielding Function;
coherence
not canGFDistinction F is empty
proof end;
end;

registration
let F be non empty Graph-yielding Function;
coherence
proof end;
end;

theorem Th83: :: GLIB_015:83
for F being non empty Graph-yielding Function
for x being Element of dom F holds . x = [:{[(),x]},(() . x):]
proof end;

theorem Th84: :: GLIB_015:84
for F being non empty Graph-yielding Function
for x being Element of dom F holds () . x = [:{[(),x]},(() . x):]
proof end;

registration
let F be non empty Graph-yielding Function;
coherence
proof end;
end;

theorem Th85: :: GLIB_015:85
for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom () st x = x9 holds
ex G being PGraphMapping of F . x,() . x9 st
( G _V = renameElementsDistinctlyFunc ((),x) & G _E = renameElementsDistinctlyFunc ((),x) & G is Disomorphism )
proof end;

theorem Th86: :: GLIB_015:86
for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom () st x = x9 holds
() . x9 is F . x -Disomorphic
proof end;

theorem Th87: :: GLIB_015:87
for F being non empty Graph-yielding Function holds F, canGFDistinction F are_Disomorphic
proof end;

theorem Th88: :: GLIB_015:88
for F1, F2 being non empty Graph-yielding Function st F1,F2 are_Disomorphic holds
canGFDistinction F1, canGFDistinction F2 are_Disomorphic
proof end;

theorem Th89: :: GLIB_015:89
for F1, F2 being non empty Graph-yielding Function st F1,F2 are_isomorphic holds
canGFDistinction F1, canGFDistinction F2 are_isomorphic
proof end;

theorem Th90: :: GLIB_015:90
for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom ()
for v, e, w being object st x = x9 & e DJoins v,w,F . x holds
[(),x,e] DJoins [(),x,v],[(),x,w],() . x9
proof end;

theorem Th91: :: GLIB_015:91
for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom ()
for v, e, w being object st x = x9 & e Joins v,w,F . x holds
[(),x,e] Joins [(),x,v],[(),x,w],() . x9
proof end;

theorem Th92: :: GLIB_015:92
for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom ()
for v9, e9, w9 being object st x = x9 & e9 DJoins v9,w9,() . x9 holds
ex v, e, w being object st
( e DJoins v,w,F . x & e9 = [(),x,e] & v9 = [(),x,v] & w9 = [(),x,w] )
proof end;

theorem Th93: :: GLIB_015:93
for F being non empty Graph-yielding Function
for x being Element of dom F
for x9 being Element of dom ()
for v9, e9, w9 being object st x = x9 & e9 Joins v9,w9,() . x9 holds
ex v, e, w being object st
( e Joins v,w,F . x & e9 = [(),x,e] & v9 = [(),x,v] & w9 = [(),x,w] )
proof end;

registration
let F be non empty Graph-yielding loopless Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non loopless Function;
coherence
not canGFDistinction F is loopless
proof end;
end;

registration
let F be non empty Graph-yielding non-multi Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non non-multi Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non-Dmulti Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non non-Dmulti Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding simple Function;
coherence by ;
end;

registration
let F be non empty Graph-yielding Dsimple Function;
coherence by Th87;
end;

registration
let F be non empty Graph-yielding acyclic Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non acyclic Function;
coherence
not canGFDistinction F is acyclic
proof end;
end;

registration
let F be non empty Graph-yielding connected Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non connected Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding Tree-like Function;
coherence by ;
end;

registration
let F be non empty Graph-yielding edgeless Function;
coherence
proof end;
end;

registration
let F be non empty Graph-yielding non edgeless Function;
coherence
not canGFDistinction F is edgeless
proof end;
end;

definition
let F be non empty Graph-yielding Function;
let z be Element of dom F;
func canGFDistinction (F,z) -> Graph-yielding Function equals :: GLIB_015:def 26
() +* (z,((F . z) | _GraphSelectors));
coherence
() +* (z,((F . z) | _GraphSelectors)) is Graph-yielding Function
proof end;
end;

:: deftheorem defines canGFDistinction GLIB_015:def 26 :
for F being non empty Graph-yielding Function
for z being Element of dom F holds canGFDistinction (F,z) = () +* (z,((F . z) | _GraphSelectors));

registration
let F be non empty Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction (F,z) -> non empty Graph-yielding ;
coherence
not canGFDistinction (F,z) is empty
;
end;

theorem Th94: :: GLIB_015:94
for F being non empty Graph-yielding Function
for z being Element of dom F holds dom F = dom (canGFDistinction (F,z))
proof end;

theorem Th95: :: GLIB_015:95
for F being non empty Graph-yielding Function
for z being Element of dom F
for G being Graph-yielding Function holds
( G = canGFDistinction (F,z) iff ( dom G = dom F & G . z = (F . z) | _GraphSelectors & ( for x being Element of dom F st x <> z holds
G . x = replaceVerticesEdges ((),()) ) ) )
proof end;

theorem Th96: :: GLIB_015:96
for F being non empty Graph-yielding Function
for z being Element of dom F holds (canGFDistinction (F,z)) . z = (F . z) | _GraphSelectors
proof end;

registration
let F be non empty Graph-yielding Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is plain
proof end;
end;

theorem Th97: :: GLIB_015:97
for F being non empty Graph-yielding Function
for z being Element of dom F holds (the_Vertices_of (canGFDistinction (F,z))) . z = () . z
proof end;

theorem Th98: :: GLIB_015:98
for F being non empty Graph-yielding Function
for x, z being Element of dom F st x <> z holds
(the_Vertices_of (canGFDistinction (F,z))) . x = . x
proof end;

theorem :: GLIB_015:99
for F being non empty Graph-yielding Function
for z being Element of dom F holds the_Vertices_of (canGFDistinction (F,z)) = +* (z,(the_Vertices_of (F . z)))
proof end;

theorem Th100: :: GLIB_015:100
for F being non empty Graph-yielding Function
for z being Element of dom F holds (the_Edges_of (canGFDistinction (F,z))) . z = () . z
proof end;

theorem Th101: :: GLIB_015:101
for F being non empty Graph-yielding Function
for x, z being Element of dom F st x <> z holds
(the_Edges_of (canGFDistinction (F,z))) . x = () . x
proof end;

theorem :: GLIB_015:102
for F being non empty Graph-yielding Function
for z being Element of dom F holds the_Edges_of (canGFDistinction (F,z)) = () +* (z,(the_Edges_of (F . z)))
proof end;

Lm4: for F being non empty Graph-yielding Function
for x, y being Element of dom F holds [:{[(),x]},(() . x):] misses the_Vertices_of (F . y)

proof end;

Lm5: for F being non empty Graph-yielding Function
for x, y being Element of dom F holds [:{[(),x]},(() . x):] misses the_Edges_of (F . y)

proof end;

registration
let F be non empty Graph-yielding Function;
let z be Element of dom F;
coherence
( canGFDistinction (F,z) is vertex-disjoint & canGFDistinction (F,z) is edge-disjoint )
proof end;
end;

theorem Th103: :: GLIB_015:103
for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z)) st x <> z & x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction (F,z)) . x9 st
( G _V = renameElementsDistinctlyFunc ((),x) & G _E = renameElementsDistinctlyFunc ((),x) & G is Disomorphism )
proof end;

theorem Th104: :: GLIB_015:104
for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z)) st x = x9 holds
(canGFDistinction (F,z)) . x9 is F . x -Disomorphic
proof end;

theorem Th105: :: GLIB_015:105
for F being non empty Graph-yielding Function
for z being Element of dom F holds F, canGFDistinction (F,z) are_Disomorphic
proof end;

theorem Th106: :: GLIB_015:106
for F being non empty Graph-yielding Function
for z being Element of dom F holds canGFDistinction F, canGFDistinction (F,z) are_Disomorphic
proof end;

theorem :: GLIB_015:107
for F1, F2 being non empty Graph-yielding Function
for z1 being Element of dom F1
for z2 being Element of dom F2 st F1,F2 are_Disomorphic holds
canGFDistinction (F1,z1), canGFDistinction (F2,z2) are_Disomorphic
proof end;

theorem :: GLIB_015:108
for F being non empty Graph-yielding Function
for z being Element of dom F
for z9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st z = z9 holds
( e DJoins v,w,F . z iff e DJoins v,w,(canGFDistinction (F,z)) . z9 )
proof end;

theorem :: GLIB_015:109
for F being non empty Graph-yielding Function
for z being Element of dom F
for z9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st z = z9 holds
( e Joins v,w,F . z iff e Joins v,w,(canGFDistinction (F,z)) . z9 )
proof end;

theorem :: GLIB_015:110
for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st x <> z & x = x9 & e DJoins v,w,F . x holds
[(),x,e] DJoins [(),x,v],[(),x,w],(canGFDistinction (F,z)) . x9
proof end;

theorem :: GLIB_015:111
for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z))
for v, e, w being object st x <> z & x = x9 & e Joins v,w,F . x holds
[(),x,e] Joins [(),x,v],[(),x,w],(canGFDistinction (F,z)) . x9
proof end;

theorem :: GLIB_015:112
for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z))
for v9, e9, w9 being object st x <> z & x = x9 & e9 DJoins v9,w9,(canGFDistinction (F,z)) . x9 holds
ex v, e, w being object st
( e DJoins v,w,F . x & e9 = [(),x,e] & v9 = [(),x,v] & w9 = [(),x,w] )
proof end;

theorem :: GLIB_015:113
for F being non empty Graph-yielding Function
for x, z being Element of dom F
for x9 being Element of dom (canGFDistinction (F,z))
for v9, e9, w9 being object st x <> z & x = x9 & e9 Joins v9,w9,(canGFDistinction (F,z)) . x9 holds
ex v, e, w being object st
( e Joins v,w,F . x & e9 = [(),x,e] & v9 = [(),x,v] & w9 = [(),x,w] )
proof end;

registration
let F be non empty Graph-yielding loopless Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is loopless
proof end;
end;

registration
let F be non empty Graph-yielding non loopless Function;
let z be Element of dom F;
coherence
not canGFDistinction (F,z) is loopless
proof end;
end;

registration
let F be non empty Graph-yielding non-multi Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is non-multi
proof end;
end;

registration
let F be non empty Graph-yielding non non-multi Function;
let z be Element of dom F;
coherence
not canGFDistinction (F,z) is non-multi
proof end;
end;

registration
let F be non empty Graph-yielding non-Dmulti Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is non-Dmulti
proof end;
end;

registration
let F be non empty Graph-yielding non non-Dmulti Function;
let z be Element of dom F;
coherence
not canGFDistinction (F,z) is non-Dmulti
proof end;
end;

registration
let F be non empty Graph-yielding simple Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is simple
;
end;

registration
let F be non empty Graph-yielding Dsimple Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is Dsimple
;
end;

registration
let F be non empty Graph-yielding acyclic Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is acyclic
proof end;
end;

registration
let F be non empty Graph-yielding non acyclic Function;
let z be Element of dom F;
cluster canGFDistinction (F,z) -> Graph-yielding non acyclic ;
coherence
not canGFDistinction (F,z) is acyclic
proof end;
end;

registration
let F be non empty Graph-yielding connected Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is connected
proof end;
end;

registration
let F be non empty Graph-yielding non connected Function;
let z be Element of dom F;
coherence
not canGFDistinction (F,z) is connected
proof end;
end;

registration
let F be non empty Graph-yielding Tree-like Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is Tree-like
;
end;

registration
let F be non empty Graph-yielding edgeless Function;
let z be Element of dom F;
coherence
canGFDistinction (F,z) is edgeless
proof end;
end;

registration
let F be non empty Graph-yielding non edgeless Function;
let z be Element of dom F;
coherence
not canGFDistinction (F,z) is edgeless
proof end;
end;

theorem Th114: :: GLIB_015:114
for G2, H being _Graph
for F being PGraphMapping of G2,H st F is directed & F is weak_SG-embedding holds
ex G1 being Supergraph of G2 st G1 is H -Disomorphic
proof end;

theorem :: GLIB_015:115
for G2, H being _Graph
for F being PGraphMapping of G2,H st F is weak_SG-embedding holds
ex G1 being Supergraph of G2 st G1 is H -isomorphic
proof end;

definition
let F be non empty Graph-yielding Function;
mode GraphSum of F -> _Graph means :Def27: :: GLIB_015:def 27
ex G9 being GraphUnion of rng () st it is G9 -Disomorphic ;
existence
ex b1 being _Graph ex G9 being GraphUnion of rng () st b1 is G9 -Disomorphic
proof end;
end;

:: deftheorem Def27 defines GraphSum GLIB_015:def 27 :
for F being non empty Graph-yielding Function
for b2 being _Graph holds
( b2 is GraphSum of F iff ex G9 being GraphUnion of rng () st b2 is G9 -Disomorphic );

theorem Th116: :: GLIB_015:116
for F being non empty Graph-yielding Function
for S being GraphSum of F
for G9 being GraphUnion of rng () holds S is G9 -Disomorphic
proof end;

theorem Th117: :: GLIB_015:117
for F1, F2 being non empty Graph-yielding Function
for S1 being GraphSum of F1
for S2 being GraphSum of F2 st F1,F2 are_Disomorphic holds
S2 is S1 -Disomorphic
proof end;

theorem :: GLIB_015:118
for F1, F2 being non empty Graph-yielding Function
for S1 being GraphSum of F1
for S2 being GraphSum of F2 st F1,F2 are_isomorphic holds
S2 is S1 -isomorphic
proof end;

theorem :: GLIB_015:119
for F being non empty Graph-yielding Function
for S1, S2 being GraphSum of F holds S2 is S1 -Disomorphic by Th117;

:: theorem
:: for F, G being non empty Graph-yielding Function, R being GraphUnionSet
:: for S being GraphUnion of R
:: st R = rng G & G,canGFDistinction(F) are_Disomorphic
:: holds S is GraphSum of F;
theorem Th120: :: GLIB_015:120
for x being object
for G being _Graph
for S being GraphSum of x .--> G holds S is G -Disomorphic
proof end;

theorem :: GLIB_015:121
for F being non empty Graph-yielding Function
for S being GraphSum of F st S is connected holds
ex x being object ex G being connected _Graph st F = x .--> G
proof end;

registration
let X be non empty set ;
existence
ex b1 being Graph-yielding ManySortedSet of X st
( not b1 is empty & b1 is vertex-disjoint & b1 is edge-disjoint )
proof end;
end;

theorem :: GLIB_015:122
for F being non empty Graph-yielding Function
for x being Element of dom F
for S being GraphSum of F ex M being PGraphMapping of F . x,S st M is strong_SG-embedding
proof end;

:: This is a possible generalization of the preceeding theorem.
:: :: A graph sum can be divided into its (direct, not isomorphic) parts.
:: theorem
:: for F1 being non empty Graph-yielding Function, S being GraphSum of F1
:: ex F2 being non empty vertex-disjoint edge-disjoint
:: Graph-yielding ManySortedSet of dom F1
:: st S is GraphUnion of rng F2 &
:: for x being Element of dom F1 holds F2.x is F1.x-Disomorphic
:: proof
:: let F1 be non empty Graph-yielding Function, S be GraphSum of F1;
:: :: construct function from dom F1 to a Disomorphism from F1.x to GFD(F1).x |H1
:: :: construct function from dom F1 to injection from GFD(F1).x into G9 |H2
:: :: the Disomorphism from G9 to S |F
:: :: set F2.x = rng (F*(H2.x)*(H1.x))
:: :: show F2.x is Disomorphism from F1.x to F2.x
:: :: show F2 is vertex-disjoint
:: :: show F2 is edge-disjoint
:: :: show S is GraphUnion
:: thus thesis;
:: end;
theorem Th123: :: GLIB_015:123
for F being non empty Graph-yielding Function
for z being Element of dom F ex S being GraphSum of F st
( S is Supergraph of F . z & S is GraphUnion of rng (canGFDistinction (F,z)) )
proof end;

theorem Th124: :: GLIB_015:124
for F being non empty Graph-yielding Function
for S being GraphSum of F holds
( ( F is loopless implies S is loopless ) & ( S is loopless implies F is loopless ) & ( F is non-multi implies S is non-multi ) & ( S is non-multi implies F is non-multi ) & ( F is non-Dmulti implies S is non-Dmulti ) & ( S is non-Dmulti implies F is non-Dmulti ) & ( F is simple implies S is simple ) & ( S is simple implies F is simple ) & ( F is Dsimple implies S is Dsimple ) & ( S is Dsimple implies F is Dsimple ) & ( F is chordal implies S is chordal ) & ( S is chordal implies F is chordal ) & ( F is edgeless implies S is edgeless ) & ( S is edgeless implies F is edgeless ) & ( F is loopfull implies S is loopfull ) & ( S is loopfull implies F is loopfull ) )
proof end;

registration
let F be non empty Graph-yielding loopless Function;
cluster -> loopless for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is loopless
by Th124;
end;

registration
let F be non empty Graph-yielding non loopless Function;
cluster -> non loopless for GraphSum of F;
coherence
for b1 being GraphSum of F holds not b1 is loopless
by Th124;
end;

registration
let F be non empty Graph-yielding non-Dmulti Function;
cluster -> non-Dmulti for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is non-Dmulti
by Th124;
end;

registration
let F be non empty Graph-yielding non non-Dmulti Function;
cluster -> non non-Dmulti for GraphSum of F;
coherence
for b1 being GraphSum of F holds not b1 is non-Dmulti
by Th124;
end;

registration
let F be non empty Graph-yielding non-multi Function;
cluster -> non-multi for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is non-multi
by Th124;
end;

registration
let F be non empty Graph-yielding non non-multi Function;
cluster -> non non-multi for GraphSum of F;
coherence
for b1 being GraphSum of F holds not b1 is non-multi
by Th124;
end;

registration
let F be non empty Graph-yielding simple Function;
cluster -> simple for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is simple
;
end;

registration
let F be non empty Graph-yielding Dsimple Function;
cluster -> Dsimple for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is Dsimple
;
end;

registration
let F be non empty Graph-yielding edgeless Function;
cluster -> edgeless for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is edgeless
by Th124;
end;

registration
let F be non empty Graph-yielding non edgeless Function;
cluster -> non edgeless for GraphSum of F;
coherence
for b1 being GraphSum of F holds not b1 is edgeless
by Th124;
end;

registration
let F be non empty Graph-yielding loopfull Function;
cluster -> loopfull for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is loopfull
by Th124;
end;

registration
let F be non empty Graph-yielding non loopfull Function;
cluster -> non loopfull for GraphSum of F;
coherence
for b1 being GraphSum of F holds not b1 is loopfull
by Th124;
end;

theorem Th125: :: GLIB_015:125
for F being non empty Graph-yielding Function
for S being GraphSum of F holds
( ( F is acyclic implies S is acyclic ) & ( S is acyclic implies F is acyclic ) & ( F is chordal implies S is chordal ) & ( S is chordal implies F is chordal ) )
proof end;

registration
let F be non empty Graph-yielding acyclic Function;
cluster -> acyclic for GraphSum of F;
coherence
for b1 being GraphSum of F holds b1 is acyclic
by Th125;
end;

registration
let F be non empty Graph-yielding non acyclic Function;
cluster -> non acyclic for GraphSum of F;
coherence
for b1 being GraphSum of F holds not b1 is acyclic
by Th125;
end;

theorem :: GLIB_015:126
for F being non empty Graph-yielding Function
for S being GraphSum of F holds card F c= S .numComponents()
proof end;

theorem :: GLIB_015:127
for F being non empty Graph-yielding connected Function
for S being GraphSum of F holds card F = S .numComponents()
proof end;

definition
let G1, G2 be _Graph;
mode GraphSum of G1,G2 -> Supergraph of G1 means :Def28: :: GLIB_015:def 28
it is GraphSum of <*G1,G2*>;
existence
ex b1 being Supergraph of G1 st b1 is GraphSum of <*G1,G2*>
proof end;
end;

:: deftheorem Def28 defines GraphSum GLIB_015:def 28 :
for G1, G2 being _Graph
for b3 being Supergraph of G1 holds
( b3 is GraphSum of G1,G2 iff b3 is GraphSum of <*G1,G2*> );

theorem Th128: :: GLIB_015:128
for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds
( ( G1 is loopless & G2 is loopless implies S is loopless ) & ( S is loopless implies ( G1 is loopless & G2 is loopless ) ) & ( G1 is non-multi & G2 is non-multi implies S is non-multi ) & ( S is non-multi implies ( G1 is non-multi & G2 is non-multi ) ) & ( G1 is non-Dmulti & G2 is non-Dmulti implies S is non-Dmulti ) & ( S is non-Dmulti implies ( G1 is non-Dmulti & G2 is non-Dmulti ) ) & ( G1 is simple & G2 is simple implies S is simple ) & ( S is simple implies ( G1 is simple & G2 is simple ) ) & ( G1 is Dsimple & G2 is Dsimple implies S is Dsimple ) & ( S is Dsimple implies ( G1 is Dsimple & G2 is Dsimple ) ) & ( G1 is acyclic & G2 is acyclic implies S is acyclic ) & ( S is acyclic implies ( G1 is acyclic & G2 is acyclic ) ) & ( G1 is chordal & G2 is chordal implies S is chordal ) & ( S is chordal implies ( G1 is chordal & G2 is chordal ) ) & ( G1 is edgeless & G2 is edgeless implies S is edgeless ) & ( S is edgeless implies ( G1 is edgeless & G2 is edgeless ) ) & ( G1 is loopfull & G2 is loopfull implies S is loopfull ) & ( S is loopfull implies ( G1 is loopfull & G2 is loopfull ) ) )
proof end;

registration
let G1, G2 be loopless _Graph;
cluster -> loopless for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is loopless
by Th128;
end;

registration
let G1, G2 be non loopless _Graph;
cluster -> non loopless for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds not b1 is loopless
;
end;

registration
let G1, G2 be non-Dmulti _Graph;
cluster -> non-Dmulti for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is non-Dmulti
by Th128;
end;

registration
let G1, G2 be non non-Dmulti _Graph;
cluster -> non non-Dmulti for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds not b1 is non-Dmulti
;
end;

registration
let G1, G2 be non-multi _Graph;
cluster -> non-multi for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is non-multi
by Th128;
end;

registration
let G1, G2 be non non-multi _Graph;
cluster -> non non-multi for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds not b1 is non-multi
;
end;

registration
let G1, G2 be simple _Graph;
cluster -> simple for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is simple
;
end;

registration
let G1, G2 be Dsimple _Graph;
cluster -> Dsimple for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is Dsimple
;
end;

registration
let G1, G2 be acyclic _Graph;
cluster -> acyclic for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is acyclic
by Th128;
end;

registration
let G1, G2 be non acyclic _Graph;
cluster -> non acyclic for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds not b1 is acyclic
;
end;

registration
let G1, G2 be edgeless _Graph;
cluster -> edgeless for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is edgeless
by Th128;
end;

registration
let G1, G2 be non edgeless _Graph;
cluster -> non edgeless for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds not b1 is edgeless
;
end;

registration
let G1, G2 be loopfull _Graph;
cluster -> loopfull for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds b1 is loopfull
by Th128;
end;

registration
let G1, G2 be non loopfull _Graph;
cluster -> non loopfull for GraphSum of G1,G2;
coherence
for b1 being GraphSum of G1,G2 holds not b1 is loopfull
by Th128;
end;

Lm6: for G1, G2 being _Graph
for G9 being GraphUnion of rng (canGFDistinction <*G1,G2*>) ex G3, G4 being _Graph st
( the_Edges_of G3 misses the_Edges_of G4 & G3 tolerates G4 & the_Vertices_of G3 misses the_Vertices_of G4 & G9 is GraphUnion of G3,G4 & G3 is G1 -Disomorphic & G4 is G2 -Disomorphic )

proof end;

theorem :: GLIB_015:129
for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds S .order() = (G1 .order()) + (G2 .order())
proof end;

theorem :: GLIB_015:130
for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds S .size() = (G1 .size()) + (G2 .size())
proof end;

theorem :: GLIB_015:131
for G1, G2 being _Graph
for S being GraphSum of G1,G2 holds S .numComponents() = () +` ()
proof end;