GLIB_015: About Graph Sums

:: About Graph Sums
:: by Sebastian Koch
::
:: Received November 30, 2021
:: 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 * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & it = createGraph ((rng V),(rng E),S,T) );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def1 defines replaceVerticesEdges GLIB_015:def 1 :

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 (the_Edges_of G)));

coherence ;

end;

:: deftheorem defines replaceVertices GLIB_015:def 2 :

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 ((id (the_Vertices_of G)),E);

coherence ;

end;

:: deftheorem defines replaceEdges GLIB_015:def 3 :

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 * (the_Source_of G)) * (E ") & the_Target_of (replaceVerticesEdges (V,E)) = (V * (the_Target_of G)) * (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 (replaceVertices V) = rng V & the_Edges_of (replaceVertices V) = the_Edges_of G & the_Source_of (replaceVertices V) = V * (the_Source_of G) & the_Target_of (replaceVertices V) = V * (the_Target_of G) )

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 (replaceEdges E) = the_Vertices_of G & the_Edges_of (replaceEdges E) = rng E & the_Source_of (replaceEdges E) = (the_Source_of G) * (E ") & the_Target_of (replaceEdges E) = (the_Target_of G) * (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;

cluster replaceVerticesEdges (V,E) -> loopless plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> loopless plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> loopless plain ;

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

proof end;

end;

registration

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

cluster replaceVertices V -> non loopless plain ;

coherence ;

end;

registration

let G be non loopless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> non loopless plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> non-multi plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> non-multi plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> non-multi plain ;

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

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;

cluster replaceVertices V -> non non-multi plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> non non-multi plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> non-Dmulti plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> non-Dmulti plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> non-Dmulti plain ;

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

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;

cluster replaceVertices V -> non non-Dmulti plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> non non-Dmulti plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> simple plain ;

coherence ;

end;

registration

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

cluster replaceVertices V -> simple plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> simple plain ;

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;

cluster replaceVerticesEdges (V,E) -> Dsimple plain ;

coherence ;

end;

registration

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

cluster replaceVertices V -> Dsimple plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> Dsimple plain ;

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;

cluster replaceVerticesEdges (V,E) -> _trivial plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> _trivial plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> _trivial plain ;

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

proof end;

end;

registration

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

cluster replaceVertices V -> non _trivial plain ;

coherence ;

end;

registration

let G be non _trivial _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> non _trivial plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> plain vertex-finite ;

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;

cluster replaceVertices V -> plain vertex-finite ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain vertex-finite ;

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;

cluster replaceVerticesEdges (V,E) -> plain non vertex-finite ;

coherence

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;

cluster replaceVertices V -> plain non vertex-finite ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain non vertex-finite ;

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;

cluster replaceVerticesEdges (V,E) -> plain edge-finite ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> plain edge-finite ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain edge-finite ;

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

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;

cluster replaceVertices V -> plain non edge-finite ;

coherence ;

end;

registration

let G be non edge-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> plain non edge-finite ;

coherence ;

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 ;

end;

registration

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

cluster replaceVertices V -> plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain ;

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;

cluster replaceVerticesEdges (V,E) -> acyclic plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> acyclic plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> acyclic plain ;

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

proof end;

end;

registration

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

cluster replaceVertices V -> non acyclic plain ;

coherence ;

end;

registration

let G be non acyclic _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> non acyclic plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> connected plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> connected plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> connected plain ;

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

proof end;

end;

registration

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

cluster replaceVertices V -> non connected plain ;

coherence ;

end;

registration

let G be non connected _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> non connected plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> Tree-like plain ;

coherence ;

end;

registration

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

cluster replaceVertices V -> Tree-like plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> Tree-like plain ;

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;

cluster replaceVerticesEdges (V,E) -> chordal plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> chordal plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> chordal plain ;

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;

cluster replaceVerticesEdges (V,E) -> edgeless plain ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> edgeless plain ;

coherence ;

end;

registration

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

cluster replaceEdges E -> edgeless plain ;

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

proof end;

end;

registration

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

cluster replaceVertices V -> non edgeless plain ;

coherence ;

end;

registration

let G be non edgeless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> non edgeless plain ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> plain loopfull ;

coherence

proof end;

end;

registration

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

cluster replaceVertices V -> plain loopfull ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain loopfull ;

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

proof end;

end;

registration

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

cluster replaceVertices V -> plain non loopfull ;

coherence ;

end;

registration

let G be non loopfull _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;

cluster replaceEdges E -> plain non loopfull ;

coherence ;

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;

cluster replaceVerticesEdges (V,E) -> plain locally-finite ;

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;

cluster replaceVertices V -> plain locally-finite ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain locally-finite ;

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;

cluster replaceVerticesEdges (V,E) -> plain non locally-finite ;

coherence

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;

cluster replaceVertices V -> plain non locally-finite ;

coherence ;

end;

registration

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

cluster replaceEdges E -> plain non locally-finite ;

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;

cluster replaceVerticesEdges (V,E) -> plain c -vertex ;

coherence

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;

cluster replaceVertices V -> plain c -vertex ;

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;

cluster replaceEdges E -> plain c -vertex ;

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;

cluster replaceVerticesEdges (V,E) -> plain c -edge ;

coherence

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;

cluster replaceVertices V -> plain c -edge ;

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;

cluster replaceEdges E -> plain c -edge ;

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 * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = 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 * (W1 .vertexSeq()) = 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 * (W1 .edgeSeq()) = 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 * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = 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 * (W1 .vertexSeq()) = 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 * (W1 .edgeSeq()) = 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

proof end;

uniqueness

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

proof end;

uniqueness

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

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines the_Vertices_of GLIB_015:def 4 :

:: deftheorem Def5 defines the_Edges_of GLIB_015:def 5 :

:: deftheorem Def6 defines the_Source_of GLIB_015:def 6 :

:: deftheorem Def7 defines the_Target_of GLIB_015:def 7 :

registration

let F be Graph-yielding Function;

cluster the_Source_of F -> Function-yielding ;

coherence

proof end;

cluster the_Target_of F -> Function-yielding ;

coherence

proof end;

end;

registration

let F be empty Graph-yielding Function;

cluster the_Vertices_of F -> empty ;

coherence

proof end;

cluster the_Edges_of F -> empty ;

coherence

proof end;

cluster the_Source_of F -> empty ;

coherence

proof end;

cluster the_Target_of F -> empty ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding Function;

cluster the_Vertices_of F -> non empty ;

coherence

proof end;

cluster the_Edges_of F -> non empty ;

coherence

proof end;

cluster the_Source_of F -> non empty ;

coherence

proof end;

cluster the_Target_of F -> non empty ;

coherence

proof end;

end;

registration

let F be Graph-yielding Function;

cluster the_Vertices_of F -> non-empty ;

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

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

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

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

proof end;

end;

:: deftheorem Def8 defines the_Vertices_of GLIB_015:def 8 :

:: deftheorem Def9 defines the_Edges_of GLIB_015:def 9 :

:: deftheorem defines the_Source_of GLIB_015:def 10 :

:: deftheorem defines the_Target_of GLIB_015:def 11 :

theorem :: GLIB_015:24

for F being Graph-yielding Function holds the_Vertices_of (rng F) = rng (the_Vertices_of F)

proof end;

theorem :: GLIB_015:25

for F being Graph-yielding Function holds the_Edges_of (rng F) = rng (the_Edges_of F)

proof end;

theorem :: GLIB_015:26

for F being Graph-yielding Function holds the_Source_of (rng F) = rng (the_Source_of F)

proof end;

theorem :: GLIB_015:27

for F being Graph-yielding Function holds the_Target_of (rng F) = rng (the_Target_of F)

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 b₂ -Disomorphic _Graph ) );

reflexivity

proof end;

symmetry

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 b₂ -isomorphic _Graph ) );

reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem defines are_Disomorphic GLIB_015:def 12 :

:: deftheorem defines are_isomorphic GLIB_015:def 13 :

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

proof end;

symmetry

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

proof end;

symmetry

proof end;

end;

:: deftheorem defines are_Disomorphic GLIB_015:def 14 :

:: deftheorem defines are_isomorphic GLIB_015:def 15 :

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;

:: might require Proof outside this article

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

proof end;

reflexivity

proof end;

symmetry

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

proof end;

reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem defines are_Disomorphic GLIB_015:def 16 :

:: deftheorem defines are_isomorphic GLIB_015:def 17 :

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 :

:: deftheorem Def19 defines edge-disjoint GLIB_015:def 19 :

:: might require Proof outside this article

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

cluster trivial Graph-membered -> Graph-membered vertex-disjoint edge-disjoint for set ;

coherence by ZFMISC_1:def 10;

cluster Graph-membered edgeless -> Graph-membered edge-disjoint for set ;

coherence

proof end;

cluster Graph-membered edge-disjoint -> Graph-membered \/-tolerating for set ;

coherence

proof end;

cluster Graph-membered \/-tolerating vertex-disjoint -> Graph-membered edge-disjoint for set ;

coherence

proof end;

end;

registration

let G be _Graph;

cluster {G} -> vertex-disjoint edge-disjoint ;

coherence ;

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

cluster non empty Graph-membered loopless non-multi non-Dmulti simple Dsimple acyclic \/-tolerating vertex-disjoint edge-disjoint for set ;

existence

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 ;

cluster the_Vertices_of S -> mutually-disjoint ;

coherence

proof end;

end;

registration

let S be Graph-membered edge-disjoint set ;

cluster the_Edges_of S -> mutually-disjoint ;

coherence

proof end;

end;

registration

let S be Graph-membered vertex-disjoint set ;

cluster -> vertex-disjoint for Element of bool S;

coherence by Def18;

end;

registration

let S1 be Graph-membered vertex-disjoint set ;
let S2 be set ;

cluster S1 /\ S2 -> vertex-disjoint ;

coherence

proof end;

cluster S1 \ S2 -> vertex-disjoint ;

coherence ;

end;

registration

let S be Graph-membered edge-disjoint set ;

cluster -> edge-disjoint for Element of bool S;

coherence by Def19;

end;

registration

let S1 be Graph-membered edge-disjoint set ;
let S2 be set ;

cluster S1 /\ S2 -> edge-disjoint ;

coherence

proof end;

cluster S1 \ S2 -> edge-disjoint ;

coherence ;

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 (the_Edges_of G2) 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 by Th60;

end;

registration

let S be non-Dmulti vertex-disjoint GraphUnionSet;

cluster -> non-Dmulti for GraphUnion of S;

coherence by Th60;

end;

registration

let S be simple vertex-disjoint GraphUnionSet;

cluster -> simple for GraphUnion of S;

coherence ;

end;

registration

let S be Dsimple vertex-disjoint GraphUnionSet;

cluster -> Dsimple for GraphUnion of S;

coherence ;

end;

registration

let S be acyclic vertex-disjoint GraphUnionSet;

cluster -> acyclic for GraphUnion of S;

coherence 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,(the_Vertices_of H)

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 { (H .componentSet()) 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 { (H .componentSet()) 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 { (H .componentSet()) where H is Element of S : verum }

proof end;

theorem Th67: :: GLIB_015:67

for S being non empty Graph-membered connected set holds { (H .componentSet()) where H is Element of S : verum } = SmallestPartition (the_Vertices_of S)

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 :

:: deftheorem Def21 defines edge-disjoint GLIB_015:def 21 :

:: note that edge-disjoint -> one-to-one doesn't hold because of edgeless graphs

registration

cluster trivial Relation-like Function-like Graph-yielding -> Graph-yielding vertex-disjoint edge-disjoint for set ;

coherence by ZFMISC_1:def 10;

cluster Relation-like Function-like Graph-yielding vertex-disjoint -> one-to-one Graph-yielding for set ;

coherence

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

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

proof end;

end;

:: deftheorem Def22 defines vertex-disjoint GLIB_015:def 22 :

:: deftheorem Def23 defines edge-disjoint GLIB_015:def 23 :

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
(the_Vertices_of F) . x1 misses (the_Vertices_of F) . 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
(the_Edges_of F) . x1 misses (the_Edges_of F) . x2 )

proof end;

:: might need Proof outside this article

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
( (the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 & (the_Edges_of F) . x1 misses (the_Edges_of F) . x2 ) )

proof end;

registration

let x be object ;
let G be _Graph;

cluster x .--> G -> vertex-disjoint edge-disjoint ;

coherence

proof end;

end;

registration

let G be _Graph;

cluster <*G*> -> vertex-disjoint edge-disjoint ;

coherence ;

end;

registration

cluster non empty Relation-like Function-like Graph-yielding vertex-disjoint edge-disjoint for set ;

existence

proof end;

end;

registration

let F be Graph-yielding vertex-disjoint Function;

cluster proj2 F -> vertex-disjoint ;

coherence

proof end;

end;

registration

let F be Graph-yielding edge-disjoint Function;

cluster proj2 F -> edge-disjoint ;

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

proof end;

end;

:: deftheorem defines renameElementsDistinctlyFunc GLIB_015:def 24 :

theorem Th78: :: GLIB_015:78

for f being Function
for x, y being object st x in dom f & y in f . x holds
(renameElementsDistinctlyFunc (f,x)) . 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 (renameElementsDistinctlyFunc (f,x)) 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 (renameElementsDistinctlyFunc (f,x)) = [:{[f,x]},(f . x):]

proof end;

theorem :: GLIB_015:81

for f being Function
for x1, x2 being object holds rng (renameElementsDistinctlyFunc (f,x1)) misses f . x2

proof end;

theorem Th82: :: GLIB_015:82

for f being Function
for x1, x2 being object st x1 <> x2 holds
rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2))

proof end;

registration

let f be Function;
let x be object ;

cluster renameElementsDistinctlyFunc (f,x) -> one-to-one ;

coherence ;

end;

registration

let f be empty Function;
let x be object ;

cluster renameElementsDistinctlyFunc (f,x) -> empty ;

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

proof end;

end;

registration

let F be non empty Graph-yielding Function;
let x be Element of dom F;

cluster renameElementsDistinctlyFunc ((the_Vertices_of F),x) -> non empty the_Vertices_of (F . x) -defined ;

coherence

proof end;

cluster renameElementsDistinctlyFunc ((the_Edges_of F),x) -> the_Edges_of (F . x) -defined ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding Function;
let x be Element of dom F;

cluster renameElementsDistinctlyFunc ((the_Vertices_of F),x) -> the_Vertices_of (F . x) -defined total for the_Vertices_of (F . x) -defined Function;

coherence

proof end;

cluster renameElementsDistinctlyFunc ((the_Edges_of F),x) -> the_Edges_of (F . x) -defined total for the_Edges_of (F . x) -defined Function;

coherence

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 ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def25 defines canGFDistinction GLIB_015:def 25 :

registration

let F be non empty Graph-yielding Function;

cluster canGFDistinction F -> non empty Graph-yielding ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding Function;

cluster canGFDistinction F -> Graph-yielding plain ;

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 (the_Vertices_of (canGFDistinction F)) . x = [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):]

proof end;

theorem Th84: :: GLIB_015:84

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

proof end;

registration

let F be non empty Graph-yielding Function;

cluster canGFDistinction F -> Graph-yielding vertex-disjoint edge-disjoint ;

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 (canGFDistinction F) st x = x9 holds
ex G being PGraphMapping of F . x,(canGFDistinction F) . x9 st
( G _V = renameElementsDistinctlyFunc ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),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 (canGFDistinction F) st x = x9 holds
(canGFDistinction F) . 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 (canGFDistinction F)
for v, e, w being object st x = x9 & e DJoins v,w,F . x holds
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . 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 (canGFDistinction F)
for v, e, w being object st x = x9 & e Joins v,w,F . x holds
[(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),x,w],(canGFDistinction F) . 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 (canGFDistinction F)
for v9, e9, w9 being object st x = x9 & e9 DJoins v9,w9,(canGFDistinction F) . x9 holds
ex v, e, w being object st
( e DJoins v,w,F . x & e9 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),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 (canGFDistinction F)
for v9, e9, w9 being object st x = x9 & e9 Joins v9,w9,(canGFDistinction F) . x9 holds
ex v, e, w being object st
( e Joins v,w,F . x & e9 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),x,w] )

proof end;

registration

let F be non empty Graph-yielding loopless Function;

cluster canGFDistinction F -> Graph-yielding loopless ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non loopless Function;

cluster canGFDistinction F -> Graph-yielding non loopless ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non-multi Function;

cluster canGFDistinction F -> Graph-yielding non-multi ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non non-multi Function;

cluster canGFDistinction F -> Graph-yielding non non-multi ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non-Dmulti Function;

cluster canGFDistinction F -> Graph-yielding non-Dmulti ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non non-Dmulti Function;

cluster canGFDistinction F -> Graph-yielding non non-Dmulti ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding simple Function;

cluster canGFDistinction F -> Graph-yielding simple ;

coherence by Th42, Th87;

end;

registration

let F be non empty Graph-yielding Dsimple Function;

cluster canGFDistinction F -> Graph-yielding Dsimple ;

coherence by Th87;

end;

registration

let F be non empty Graph-yielding acyclic Function;

cluster canGFDistinction F -> Graph-yielding acyclic ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non acyclic Function;

cluster canGFDistinction F -> Graph-yielding non acyclic ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding connected Function;

cluster canGFDistinction F -> Graph-yielding connected ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non connected Function;

cluster canGFDistinction F -> Graph-yielding non connected ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding Tree-like Function;

cluster canGFDistinction F -> Graph-yielding Tree-like ;

coherence by Th42, Th87;

end;

registration

let F be non empty Graph-yielding edgeless Function;

cluster canGFDistinction F -> Graph-yielding edgeless ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non edgeless Function;

cluster canGFDistinction F -> Graph-yielding non edgeless ;

coherence

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
(canGFDistinction F) +* (z,((F . z) | _GraphSelectors));

coherence

proof end;

end;

:: deftheorem defines canGFDistinction GLIB_015:def 26 :

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 ;

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 ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) ) )

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;

cluster canGFDistinction (F,z) -> Graph-yielding plain ;

coherence

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 = (the_Vertices_of F) . 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 = (the_Vertices_of (canGFDistinction F)) . 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)) = (the_Vertices_of (canGFDistinction F)) +* (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 = (the_Edges_of F) . 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 = (the_Edges_of (canGFDistinction F)) . 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)) = (the_Edges_of (canGFDistinction F)) +* (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 [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . 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 [:{[(the_Edges_of F),x]},((the_Edges_of F) . 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;

cluster canGFDistinction (F,z) -> Graph-yielding vertex-disjoint edge-disjoint ;

coherence

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 ((the_Vertices_of F),x) & G _E = renameElementsDistinctlyFunc ((the_Edges_of F),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
[(the_Edges_of F),x,e] DJoins [(the_Vertices_of F),x,v],[(the_Vertices_of F),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
[(the_Edges_of F),x,e] Joins [(the_Vertices_of F),x,v],[(the_Vertices_of F),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 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),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 = [(the_Edges_of F),x,e] & v9 = [(the_Vertices_of F),x,v] & w9 = [(the_Vertices_of F),x,w] )

proof end;

registration

let F be non empty Graph-yielding loopless Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding loopless ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non loopless Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non loopless ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non-multi Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non-multi ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non non-multi Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non non-multi ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non-Dmulti Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non-Dmulti ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non non-Dmulti Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non non-Dmulti ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding simple Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding simple ;

coherence ;

end;

registration

let F be non empty Graph-yielding Dsimple Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding Dsimple ;

coherence ;

end;

registration

let F be non empty Graph-yielding acyclic Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding acyclic ;

coherence

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

proof end;

end;

registration

let F be non empty Graph-yielding connected Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding connected ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non connected Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non connected ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding Tree-like Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding Tree-like ;

coherence ;

end;

registration

let F be non empty Graph-yielding edgeless Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding edgeless ;

coherence

proof end;

end;

registration

let F be non empty Graph-yielding non edgeless Function;
let z be Element of dom F;

cluster canGFDistinction (F,z) -> Graph-yielding non edgeless ;

coherence

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 (canGFDistinction F) st it is G9 -Disomorphic ;

existence

proof end;

end;

:: deftheorem Def27 defines GraphSum GLIB_015:def 27 :

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 (canGFDistinction F) 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 ;

cluster non empty Relation-like X -defined Function-like total Graph-yielding vertex-disjoint edge-disjoint for set ;

existence

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 by Th124;

end;

registration

let F be non empty Graph-yielding non loopless Function;

cluster -> non loopless for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding non-Dmulti Function;

cluster -> non-Dmulti for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding non non-Dmulti Function;

cluster -> non non-Dmulti for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding non-multi Function;

cluster -> non-multi for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding non non-multi Function;

cluster -> non non-multi for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding simple Function;

cluster -> simple for GraphSum of F;

coherence ;

end;

registration

let F be non empty Graph-yielding Dsimple Function;

cluster -> Dsimple for GraphSum of F;

coherence ;

end;

registration

let F be non empty Graph-yielding edgeless Function;

cluster -> edgeless for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding non edgeless Function;

cluster -> non edgeless for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding loopfull Function;

cluster -> loopfull for GraphSum of F;

coherence by Th124;

end;

registration

let F be non empty Graph-yielding non loopfull Function;

cluster -> non loopfull for GraphSum of F;

coherence 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 by Th125;

end;

registration

let F be non empty Graph-yielding non acyclic Function;

cluster -> non acyclic for GraphSum of F;

coherence 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

proof end;

end;

:: deftheorem Def28 defines GraphSum GLIB_015:def 28 :

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;