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

ex b_{1} being plain _Graph 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 ") & b_{1} = createGraph ((rng V),(rng E),S,T) )

for b_{1}, b_{2} being plain _Graph st 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 ") & b_{1} = createGraph ((rng V),(rng E),S,T) ) & 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 ") & b_{2} = createGraph ((rng V),(rng E),S,T) ) holds

b_{1} = b_{2}
;

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

ex b

( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & b

proof end;

uniqueness for b

( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & b

( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & b

b

:: 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 b_{4} being plain _Graph holds

( b_{4} = replaceVerticesEdges (V,E) iff 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 ") & b_{4} = createGraph ((rng V),(rng E),S,T) ) );

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 b

( b

( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & b

definition

let G be _Graph;

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

replaceVerticesEdges (V,(id (the_Edges_of G))) is plain _Graph ;

end;
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 replaceVerticesEdges (V,(id (the_Edges_of G)));

replaceVerticesEdges (V,(id (the_Edges_of G))) is plain _Graph ;

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

for G being _Graph

for V being non empty one-to-one ManySortedSet of the_Vertices_of G holds replaceVertices V = replaceVerticesEdges (V,(id (the_Edges_of G)));

definition

let G be _Graph;

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

replaceVerticesEdges ((id (the_Vertices_of G)),E) is plain _Graph ;

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

replaceVerticesEdges ((id (the_Vertices_of G)),E) is plain _Graph ;

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

for G being _Graph

for E being one-to-one ManySortedSet of the_Edges_of G holds replaceEdges E = replaceVerticesEdges ((id (the_Vertices_of G)),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 * (the_Source_of G)) * (E ") & the_Target_of (replaceVerticesEdges (V,E)) = (V * (the_Target_of G)) * (E ") )

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

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

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)

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

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

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)

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

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

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

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

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

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

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

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

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 )

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

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

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

registration

let G be loopless _Graph;

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

coherence

replaceVertices V is loopless ;

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

coherence

replaceVertices V is loopless ;

registration

let G be loopless _Graph;

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

coherence

replaceEdges E is loopless ;

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

coherence

replaceEdges E is loopless ;

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;

coherence

not replaceVerticesEdges (V,E) is loopless

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is loopless ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is loopless ;

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

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

registration

let G be non-multi _Graph;

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

coherence

replaceVertices V is non-multi ;

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

coherence

replaceVertices V is non-multi ;

registration

let G be non-multi _Graph;

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

coherence

replaceEdges E is non-multi ;

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

coherence

replaceEdges E is non-multi ;

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;

coherence

not replaceVerticesEdges (V,E) is non-multi

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is non-multi ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is non-multi ;

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

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

registration

let G be non-Dmulti _Graph;

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

coherence

replaceVertices V is non-Dmulti ;

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

coherence

replaceVertices V is non-Dmulti ;

registration

let G be non-Dmulti _Graph;

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

coherence

replaceEdges E is non-Dmulti ;

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

coherence

replaceEdges E is non-Dmulti ;

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;

coherence

not replaceVerticesEdges (V,E) is non-Dmulti

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

proof end;

registration

let G be non non-Dmulti _Graph;

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

coherence

not replaceVertices V is non-Dmulti ;

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

coherence

not replaceVertices V is non-Dmulti ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is non-Dmulti ;

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

registration

let G be simple _Graph;

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

coherence

replaceVertices V is simple ;

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

coherence

replaceVertices V is simple ;

registration

let G be simple _Graph;

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

coherence

replaceEdges E is simple ;

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

coherence

replaceEdges E is simple ;

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

registration

let G be Dsimple _Graph;

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

coherence

replaceVertices V is Dsimple ;

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

coherence

replaceVertices V is Dsimple ;

registration

let G be Dsimple _Graph;

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

coherence

replaceEdges E is Dsimple ;

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

coherence

replaceEdges E is Dsimple ;

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

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

registration

let G be _trivial _Graph;

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

coherence

replaceVertices V is _trivial ;

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

coherence

replaceVertices V is _trivial ;

registration

let G be _trivial _Graph;

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

coherence

replaceEdges E is _trivial ;

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

coherence

replaceEdges E is _trivial ;

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;

coherence

not replaceVerticesEdges (V,E) is _trivial

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is _trivial ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is _trivial ;

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

replaceVerticesEdges (V,E) is vertex-finite

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

proof end;

registration

let G be vertex-finite _Graph;

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

coherence

replaceVertices V is vertex-finite ;

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

coherence

replaceVertices V is vertex-finite ;

registration

let G be vertex-finite _Graph;

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

coherence

replaceEdges E is vertex-finite ;

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

coherence

replaceEdges E is vertex-finite ;

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

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

registration

let G be non vertex-finite _Graph;

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

coherence

not replaceVertices V is vertex-finite ;

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

coherence

not replaceVertices V is vertex-finite ;

registration

let G be non vertex-finite _Graph;

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

coherence

not replaceEdges E is vertex-finite ;

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

coherence

not replaceEdges E is vertex-finite ;

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

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

registration

let G be edge-finite _Graph;

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

coherence

replaceVertices V is edge-finite ;

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

coherence

replaceVertices V is edge-finite ;

registration

let G be edge-finite _Graph;

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

coherence

replaceEdges E is edge-finite ;

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

coherence

replaceEdges E is edge-finite ;

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;

coherence

not replaceVerticesEdges (V,E) is edge-finite

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

proof end;

registration

let G be non edge-finite _Graph;

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

coherence

not replaceVertices V is edge-finite ;

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

coherence

not replaceVertices V is edge-finite ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is edge-finite ;

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;

coherence

replaceVerticesEdges (V,E) is finite ;

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

registration

let G be _Graph;

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

coherence

replaceVertices V is finite ;

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

coherence

replaceVertices V is finite ;

registration

let G be _Graph;

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

coherence

replaceEdges E is finite ;

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

coherence

replaceEdges E is finite ;

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

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

registration

let G be acyclic _Graph;

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

coherence

replaceVertices V is acyclic ;

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

coherence

replaceVertices V is acyclic ;

registration

let G be acyclic _Graph;

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

coherence

replaceEdges E is acyclic ;

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

coherence

replaceEdges E is acyclic ;

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;

coherence

not replaceVerticesEdges (V,E) is acyclic

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is acyclic ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is acyclic ;

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

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

registration

let G be connected _Graph;

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

coherence

replaceVertices V is connected ;

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

coherence

replaceVertices V is connected ;

registration

let G be connected _Graph;

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

coherence

replaceEdges E is connected ;

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

coherence

replaceEdges E is connected ;

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;

coherence

not replaceVerticesEdges (V,E) is connected

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is connected ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is connected ;

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

registration

let G be Tree-like _Graph;

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

coherence

replaceVertices V is Tree-like ;

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

coherence

replaceVertices V is Tree-like ;

registration

let G be Tree-like _Graph;

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

coherence

replaceEdges E is Tree-like ;

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

coherence

replaceEdges E is Tree-like ;

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

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

registration

let G be chordal _Graph;

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

coherence

replaceVertices V is chordal ;

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

coherence

replaceVertices V is chordal ;

registration

let G be chordal _Graph;

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

coherence

replaceEdges E is chordal ;

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

coherence

replaceEdges E is chordal ;

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

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

registration

let G be edgeless _Graph;

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

coherence

replaceVertices V is edgeless ;

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

coherence

replaceVertices V is edgeless ;

registration

let G be edgeless _Graph;

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

coherence

replaceEdges E is edgeless ;

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

coherence

replaceEdges E is edgeless ;

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;

coherence

not replaceVerticesEdges (V,E) is edgeless

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is edgeless ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is edgeless ;

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

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

registration

let G be loopfull _Graph;

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

coherence

replaceVertices V is loopfull ;

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

coherence

replaceVertices V is loopfull ;

registration

let G be loopfull _Graph;

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

coherence

replaceEdges E is loopfull ;

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

coherence

replaceEdges E is loopfull ;

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;

coherence

not replaceVerticesEdges (V,E) is loopfull

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

proof 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;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;

coherence

not replaceVertices V is loopfull ;

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;
let E be one-to-one ManySortedSet of the_Edges_of G;

coherence

not replaceEdges E is loopfull ;

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

replaceVerticesEdges (V,E) is locally-finite

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

proof end;

registration

let G be locally-finite _Graph;

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

coherence

replaceVertices V is locally-finite ;

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

coherence

replaceVertices V is locally-finite ;

registration

let G be locally-finite _Graph;

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

coherence

replaceEdges E is locally-finite ;

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

coherence

replaceEdges E is locally-finite ;

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

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

registration

let G be non locally-finite _Graph;

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

coherence

not replaceVertices V is locally-finite ;

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

coherence

not replaceVertices V is locally-finite ;

registration

let G be non locally-finite _Graph;

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

coherence

not replaceEdges E is locally-finite ;

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

coherence

not replaceEdges E is locally-finite ;

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

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

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

replaceVertices V is c -vertex ;

end;
let G be c -vertex _Graph;

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

coherence

replaceVertices V is c -vertex ;

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

replaceEdges E is c -vertex ;

end;
let G be c -vertex _Graph;

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

coherence

replaceEdges E is c -vertex ;

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

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

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

replaceVertices V is c -edge ;

end;
let G be c -edge _Graph;

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

coherence

replaceVertices V is c -edge ;

registration

let c be Cardinal;

let G be c -edge _Graph;

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

coherence

replaceEdges E is c -edge ;

end;
let G be c -edge _Graph;

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

coherence

replaceEdges E is c -edge ;

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

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

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

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

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

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

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;

ex b_{1} being Function st

( dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Vertices_of G ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Vertices_of G ) ) & dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Vertices_of G ) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Edges_of G ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Edges_of G ) ) & dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Edges_of G ) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Source_of G ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Source_of G ) ) & dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Source_of G ) ) holds

b_{1} = b_{2}

ex b_{1} being Function st

( dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Target_of G ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{1} . x = the_Target_of G ) ) & dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Target_of G ) ) holds

b_{1} = b_{2}

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

ex b

( dom b

ex G being _Graph st

( G = F . x & b

proof end;

uniqueness for b

ex G being _Graph st

( G = F . x & b

ex G being _Graph st

( G = F . x & b

b

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

ex b

( dom b

ex G being _Graph st

( G = F . x & b

proof end;

uniqueness for b

ex G being _Graph st

( G = F . x & b

ex G being _Graph st

( G = F . x & b

b

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

ex b

( dom b

ex G being _Graph st

( G = F . x & b

proof end;

uniqueness for b

ex G being _Graph st

( G = F . x & b

ex G being _Graph st

( G = F . x & b

b

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

ex b

( dom b

ex G being _Graph st

( G = F . x & b

proof end;

uniqueness for b

ex G being _Graph st

( G = F . x & b

ex G being _Graph st

( G = F . x & b

b

proof end;

:: deftheorem Def4 defines the_Vertices_of GLIB_015:def 4 :

for F being Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Vertices_of F iff ( dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Vertices_of G ) ) ) );

for F being Graph-yielding Function

for b

( b

ex G being _Graph st

( G = F . x & b

:: deftheorem Def5 defines the_Edges_of GLIB_015:def 5 :

for F being Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Edges_of F iff ( dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Edges_of G ) ) ) );

for F being Graph-yielding Function

for b

( b

ex G being _Graph st

( G = F . x & b

:: deftheorem Def6 defines the_Source_of GLIB_015:def 6 :

for F being Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Source_of F iff ( dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Source_of G ) ) ) );

for F being Graph-yielding Function

for b

( b

ex G being _Graph st

( G = F . x & b

:: deftheorem Def7 defines the_Target_of GLIB_015:def 7 :

for F being Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Target_of F iff ( dom b_{2} = dom F & ( for x being object st x in dom F holds

ex G being _Graph st

( G = F . x & b_{2} . x = the_Target_of G ) ) ) );

for F being Graph-yielding Function

for b

( b

ex G being _Graph st

( G = F . x & b

registration

let F be Graph-yielding Function;

coherence

the_Source_of F is Function-yielding

the_Target_of F is Function-yielding

end;
coherence

the_Source_of F is Function-yielding

proof end;

coherence the_Target_of F is Function-yielding

proof end;

registration

let F be empty Graph-yielding Function;

coherence

the_Vertices_of F is empty

the_Edges_of F is empty

the_Source_of F is empty

the_Target_of F is empty

end;
coherence

the_Vertices_of F is empty

proof end;

coherence the_Edges_of F is empty

proof end;

coherence the_Source_of F is empty

proof end;

coherence the_Target_of F is empty

proof end;

registration

let F be non empty Graph-yielding Function;

coherence

not the_Vertices_of F is empty

not the_Edges_of F is empty

not the_Source_of F is empty

not the_Target_of F is empty

end;
coherence

not the_Vertices_of F is empty

proof end;

coherence not the_Edges_of F is empty

proof end;

coherence not the_Source_of F is empty

proof end;

coherence not the_Target_of F is empty

proof end;

registration
end;

definition

let F be non empty Graph-yielding Function;

for b_{1} being Function holds

( b_{1} = the_Vertices_of F iff ( dom b_{1} = dom F & ( for x being Element of dom F holds b_{1} . x = the_Vertices_of (F . x) ) ) )

for b_{1} being Function holds

( b_{1} = the_Edges_of F iff ( dom b_{1} = dom F & ( for x being Element of dom F holds b_{1} . x = the_Edges_of (F . x) ) ) )

for b_{1} being Function holds

( b_{1} = the_Source_of F iff ( dom b_{1} = dom F & ( for x being Element of dom F holds b_{1} . x = the_Source_of (F . x) ) ) )

for b_{1} being Function holds

( b_{1} = the_Target_of F iff ( dom b_{1} = dom F & ( for x being Element of dom F holds b_{1} . x = the_Target_of (F . x) ) ) )

end;
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 ( dom it = dom F & ( for x being Element of dom F holds it . x = the_Vertices_of (F . x) ) );

for b

( b

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 ( dom it = dom F & ( for x being Element of dom F holds it . x = the_Edges_of (F . x) ) );

for b

( b

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 ( dom it = dom F & ( for x being Element of dom F holds it . x = the_Source_of (F . x) ) );

for b

( b

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 ( dom it = dom F & ( for x being Element of dom F holds it . x = the_Target_of (F . x) ) );

for b

( b

proof end;

:: deftheorem Def8 defines the_Vertices_of GLIB_015:def 8 :

for F being non empty Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Vertices_of F iff ( dom b_{2} = dom F & ( for x being Element of dom F holds b_{2} . x = the_Vertices_of (F . x) ) ) );

for F being non empty Graph-yielding Function

for b

( b

:: deftheorem Def9 defines the_Edges_of GLIB_015:def 9 :

for F being non empty Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Edges_of F iff ( dom b_{2} = dom F & ( for x being Element of dom F holds b_{2} . x = the_Edges_of (F . x) ) ) );

for F being non empty Graph-yielding Function

for b

( b

:: deftheorem defines the_Source_of GLIB_015:def 10 :

for F being non empty Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Source_of F iff ( dom b_{2} = dom F & ( for x being Element of dom F holds b_{2} . x = the_Source_of (F . x) ) ) );

for F being non empty Graph-yielding Function

for b

( b

:: deftheorem defines the_Target_of GLIB_015:def 11 :

for F being non empty Graph-yielding Function

for b_{2} being Function holds

( b_{2} = the_Target_of F iff ( dom b_{2} = dom F & ( for x being Element of dom F holds b_{2} . x = the_Target_of (F . x) ) ) );

for F being non empty Graph-yielding Function

for b

( b

definition

let S1, S2 be Graph-membered set ;

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 b_{3} -Disomorphic _Graph ) )

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 b_{4} -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 b_{4} -Disomorphic _Graph ) )

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 b_{3} -isomorphic _Graph ) )

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 b_{4} -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 b_{4} -isomorphic _Graph ) )

end;
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_{2} -Disomorphic _Graph ) );

reflexivity 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

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 b

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 b

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 b

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_{2} -isomorphic _Graph ) );

reflexivity 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

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 b

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 b

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 b

proof 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 b_{4} -Disomorphic _Graph ) ) );

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 b

:: 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 b_{4} -isomorphic _Graph ) ) );

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 b

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

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

S1,S3 are_isomorphic

proof end;

theorem :: GLIB_015:31

theorem :: GLIB_015:32

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

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

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

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

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

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

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

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

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

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;

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

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

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

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

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

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

F1,F3 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 ) ;

( F1,F2 are_Disomorphic & F1,F2 are_isomorphic ) ;

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 )

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 )

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

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

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

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

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 )

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 )

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

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 )

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 )

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

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

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

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

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

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 ;

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

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;

for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2 holds

the_Edges_of G1 misses the_Edges_of G2;

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

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

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

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

( ( 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 b_{1} being Graph-membered set st b_{1} is trivial holds

( b_{1} is vertex-disjoint & b_{1} is edge-disjoint )
by ZFMISC_1:def 10;

coherence

for b_{1} being Graph-membered set st b_{1} is edgeless holds

b_{1} is edge-disjoint

for b_{1} being Graph-membered set st b_{1} is edge-disjoint holds

b_{1} is \/-tolerating

for b_{1} being Graph-membered set st b_{1} is vertex-disjoint & b_{1} is \/-tolerating holds

b_{1} is edge-disjoint

end;
for b

( b

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

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

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

( {G1,G2} is edge-disjoint iff ( G1 = G2 or the_Edges_of G1 misses the_Edges_of G2 ) )

proof end;

registration

ex b_{1} being Graph-membered set st

( not b_{1} is empty & b_{1} is \/-tolerating & b_{1} is vertex-disjoint & b_{1} is edge-disjoint & b_{1} is acyclic & b_{1} is simple & b_{1} is Dsimple & b_{1} is loopless & b_{1} is non-multi & b_{1} is non-Dmulti )
end;

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

existence ex b

( not b

proof end;

:: note that the other direction does not work,

:: for example take S = {G,H} with G == H <> G

:: for example take S = {G,H} with G == H <> G

registration

let S be Graph-membered vertex-disjoint set ;

coherence

the_Vertices_of S is mutually-disjoint

end;
coherence

the_Vertices_of S is mutually-disjoint

proof end;

registration

let S be Graph-membered edge-disjoint set ;

coherence

the_Edges_of S is mutually-disjoint

end;
coherence

the_Edges_of S is mutually-disjoint

proof end;

registration

let S be Graph-membered vertex-disjoint set ;

coherence

for b_{1} being Subset of S holds b_{1} is vertex-disjoint
by Def18;

end;
coherence

for b

registration

let S1 be Graph-membered vertex-disjoint set ;

let S2 be set ;

coherence

S1 /\ S2 is vertex-disjoint

S1 \ S2 is vertex-disjoint ;

end;
let S2 be set ;

coherence

S1 /\ S2 is vertex-disjoint

proof end;

coherence S1 \ S2 is vertex-disjoint ;

registration

let S be Graph-membered edge-disjoint set ;

coherence

for b_{1} being Subset of S holds b_{1} is edge-disjoint
by Def19;

end;
coherence

for b

registration

let S1 be Graph-membered edge-disjoint set ;

let S2 be set ;

coherence

S1 /\ S2 is edge-disjoint

S1 \ S2 is edge-disjoint ;

end;
let S2 be set ;

coherence

S1 /\ S2 is edge-disjoint

proof end;

coherence S1 \ S2 is edge-disjoint ;

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 )

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

( 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

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 )

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

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

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}

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

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

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;

coherence

for b_{1} being GraphUnion of S holds b_{1} is non-multi
by Th60;

end;
coherence

for b

registration

let S be non-Dmulti vertex-disjoint GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is non-Dmulti
by Th60;

end;
coherence

for b

registration

let S be simple vertex-disjoint GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is simple
;

end;
coherence

for b

registration

let S be Dsimple vertex-disjoint GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is Dsimple
;

end;
coherence

for b

registration

let S be acyclic vertex-disjoint GraphUnionSet;

coherence

for b_{1} being GraphUnion of S holds b_{1} is acyclic
by Th60;

end;
coherence

for b

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)

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

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

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 }

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

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

for G being GraphUnion of S st S is connected holds

card S = G .numComponents()

proof end;

definition

let F be Graph-yielding Function;

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

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

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

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

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

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

for b_{1} being Graph-yielding Function st b_{1} is trivial holds

( b_{1} is vertex-disjoint & b_{1} is edge-disjoint )
by ZFMISC_1:def 10;

for b_{1} being Graph-yielding Function st b_{1} is vertex-disjoint holds

b_{1} is one-to-one
end;

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

coherence for b

( b

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

coherence for b

b

proof end;

definition

let F be non empty Graph-yielding Function;

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

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

end;
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 for x1, x2 being Element of dom F st x1 <> x2 holds

the_Vertices_of (F . x1) misses the_Vertices_of (F . x2);

( 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 for x1, x2 being Element of dom F st x1 <> x2 holds

the_Edges_of (F . x1) misses the_Edges_of (F . x2);

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

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

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

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

(the_Vertices_of F) . x1 misses (the_Vertices_of F) . x2 )

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

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

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

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

coherence

( x .--> G is vertex-disjoint & x .--> G is edge-disjoint )

end;
let G be _Graph;

coherence

( x .--> G is vertex-disjoint & x .--> G is edge-disjoint )

proof end;

registration
end;

registration

ex b_{1} being Graph-yielding Function st

( not b_{1} is empty & b_{1} is vertex-disjoint & b_{1} is edge-disjoint )
end;

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

existence ex b

( not b

proof end;

registration
end;

registration
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

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

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 )

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

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

<:((f . x) --> [f,x]),(id (f . x)):> is ManySortedSet of f . x

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

<:((f . x) --> [f,x]),(id (f . x)):> is ManySortedSet of f . x

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

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

(renameElementsDistinctlyFunc (f,x)) . y = [f,x,y]

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

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

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

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

for x1, x2 being object st x1 <> x2 holds

rng (renameElementsDistinctlyFunc (f,x1)) misses rng (renameElementsDistinctlyFunc (f,x2))

proof end;

registration
end;

registration
end;

registration

let f be non empty non-empty Function;

let x be Element of dom f;

coherence

not renameElementsDistinctlyFunc (f,x) is empty

end;
let x be Element of dom f;

coherence

not renameElementsDistinctlyFunc (f,x) is empty

proof end;

registration

let F be non empty Graph-yielding Function;

let x be Element of dom F;

( not renameElementsDistinctlyFunc ((the_Vertices_of F),x) is empty & renameElementsDistinctlyFunc ((the_Vertices_of F),x) is the_Vertices_of (F . x) -defined )

renameElementsDistinctlyFunc ((the_Edges_of F),x) is the_Edges_of (F . x) -defined

end;
let x be Element of dom F;

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

coherence ( not renameElementsDistinctlyFunc ((the_Vertices_of F),x) is empty & renameElementsDistinctlyFunc ((the_Vertices_of F),x) is the_Vertices_of (F . x) -defined )

proof end;

coherence renameElementsDistinctlyFunc ((the_Edges_of F),x) is the_Edges_of (F . x) -defined

proof end;

registration

let F be non empty Graph-yielding Function;

let x be Element of dom F;

for b_{1} being the_Vertices_of (F . x) -defined Function st b_{1} = renameElementsDistinctlyFunc ((the_Vertices_of F),x) holds

b_{1} is total

for b_{1} being the_Edges_of (F . x) -defined Function st b_{1} = renameElementsDistinctlyFunc ((the_Edges_of F),x) holds

b_{1} is total

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

b

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 for b

b

proof end;

definition

let F be non empty Graph-yielding Function;

ex b_{1} being Graph-yielding Function st

( dom b_{1} = dom F & ( for x being Element of dom F holds b_{1} . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) )

for b_{1}, b_{2} being Graph-yielding Function st dom b_{1} = dom F & ( for x being Element of dom F holds b_{1} . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) & dom b_{2} = dom F & ( for x being Element of dom F holds b_{2} . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) holds

b_{1} = b_{2}

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

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def25 defines canGFDistinction GLIB_015:def 25 :

for F being non empty Graph-yielding Function

for b_{2} being Graph-yielding Function holds

( b_{2} = canGFDistinction F iff ( dom b_{2} = dom F & ( for x being Element of dom F holds b_{2} . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) ) );

for F being non empty Graph-yielding Function

for b

( b

registration
end;

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

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

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;

coherence

( canGFDistinction F is vertex-disjoint & canGFDistinction F is edge-disjoint )

end;
coherence

( canGFDistinction F is vertex-disjoint & canGFDistinction F is edge-disjoint )

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

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

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

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

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

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

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

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

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;

coherence

canGFDistinction F is loopless

end;
coherence

canGFDistinction F is loopless

proof end;

registration

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

coherence

not canGFDistinction F is loopless

end;
coherence

not canGFDistinction F is loopless

proof end;

registration

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

coherence

canGFDistinction F is non-multi

end;
coherence

canGFDistinction F is non-multi

proof end;

registration

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

coherence

not canGFDistinction F is non-multi

end;
coherence

not canGFDistinction F is non-multi

proof end;

registration

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

coherence

canGFDistinction F is non-Dmulti

end;
coherence

canGFDistinction F is non-Dmulti

proof end;

registration

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

coherence

not canGFDistinction F is non-Dmulti

end;
coherence

not canGFDistinction F is non-Dmulti

proof end;

registration

let F be non empty Graph-yielding simple Function;

coherence

canGFDistinction F is simple by Th42, Th87;

end;
coherence

canGFDistinction F is simple by Th42, Th87;

registration

let F be non empty Graph-yielding Dsimple Function;

coherence

canGFDistinction F is Dsimple by Th87;

end;
coherence

canGFDistinction F is Dsimple by Th87;

registration

let F be non empty Graph-yielding acyclic Function;

coherence

canGFDistinction F is acyclic

end;
coherence

canGFDistinction F is acyclic

proof end;

registration

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

coherence

not canGFDistinction F is acyclic

end;
coherence

not canGFDistinction F is acyclic

proof end;

registration

let F be non empty Graph-yielding connected Function;

coherence

canGFDistinction F is connected

end;
coherence

canGFDistinction F is connected

proof end;

registration

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

coherence

not canGFDistinction F is connected

end;
coherence

not canGFDistinction F is connected

proof end;

registration

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

coherence

canGFDistinction F is Tree-like by Th42, Th87;

end;
coherence

canGFDistinction F is Tree-like by Th42, Th87;

registration

let F be non empty Graph-yielding edgeless Function;

coherence

canGFDistinction F is edgeless

end;
coherence

canGFDistinction F is edgeless

proof end;

registration

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

coherence

not canGFDistinction F is edgeless

end;
coherence

not canGFDistinction F is edgeless

proof end;

definition

let F be non empty Graph-yielding Function;

let z be Element of dom F;

(canGFDistinction F) +* (z,((F . z) | _GraphSelectors)) is Graph-yielding Function

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

(canGFDistinction F) +* (z,((F . z) | _GraphSelectors)) is Graph-yielding Function

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

for F being non empty Graph-yielding Function

for z being Element of dom F holds canGFDistinction (F,z) = (canGFDistinction F) +* (z,((F . z) | _GraphSelectors));

registration

let F be non empty Graph-yielding Function;

let z be Element of dom F;

coherence

not canGFDistinction (F,z) is empty ;

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is empty ;

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

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

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

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

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is plain

proof 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

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

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

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

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

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

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;

coherence

( canGFDistinction (F,z) is vertex-disjoint & canGFDistinction (F,z) is edge-disjoint )

end;
let z be Element of dom F;

coherence

( canGFDistinction (F,z) is vertex-disjoint & canGFDistinction (F,z) is edge-disjoint )

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

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

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

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

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

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 )

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 )

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

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

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

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

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;

coherence

canGFDistinction (F,z) is loopless

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is loopless

proof 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

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is loopless

proof 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

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is non-multi

proof 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

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is non-multi

proof 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

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is non-Dmulti

proof 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

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is non-Dmulti

proof 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;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is simple ;

registration

let F be non empty Graph-yielding Dsimple Function;

let z be Element of dom F;

coherence

canGFDistinction (F,z) is Dsimple ;

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is Dsimple ;

registration

let F be non empty Graph-yielding acyclic Function;

let z be Element of dom F;

coherence

canGFDistinction (F,z) is acyclic

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is acyclic

proof end;

registration

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

let z be Element of dom F;

coherence

not canGFDistinction (F,z) is acyclic

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is acyclic

proof end;

registration

let F be non empty Graph-yielding connected Function;

let z be Element of dom F;

coherence

canGFDistinction (F,z) is connected

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is connected

proof 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

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is connected

proof 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;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is Tree-like ;

registration

let F be non empty Graph-yielding edgeless Function;

let z be Element of dom F;

coherence

canGFDistinction (F,z) is edgeless

end;
let z be Element of dom F;

coherence

canGFDistinction (F,z) is edgeless

proof 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

end;
let z be Element of dom F;

coherence

not canGFDistinction (F,z) is edgeless

proof 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

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

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;

ex b_{1} being _Graph ex G9 being GraphUnion of rng (canGFDistinction F) st b_{1} is G9 -Disomorphic

end;
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 ex G9 being GraphUnion of rng (canGFDistinction F) st it is G9 -Disomorphic ;

ex b

proof end;

:: deftheorem Def27 defines GraphSum GLIB_015:def 27 :

for F being non empty Graph-yielding Function

for b_{2} being _Graph holds

( b_{2} is GraphSum of F iff ex G9 being GraphUnion of rng (canGFDistinction F) st b_{2} is G9 -Disomorphic );

for F being non empty Graph-yielding Function

for b

( b

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

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

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

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;

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;

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

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 ;

ex b_{1} being Graph-yielding ManySortedSet of X st

( not b_{1} is empty & b_{1} is vertex-disjoint & b_{1} is edge-disjoint )

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

existence ex b

( not b

proof 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

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;

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

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

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;

coherence

for b_{1} being GraphSum of F holds b_{1} is loopless
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds not b_{1} is loopless
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds b_{1} is non-Dmulti
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds not b_{1} is non-Dmulti
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds b_{1} is non-multi
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds not b_{1} is non-multi
by Th124;

end;
coherence

for b

registration

let F be non empty Graph-yielding simple Function;

coherence

for b_{1} being GraphSum of F holds b_{1} is simple
;

end;
coherence

for b

registration

let F be non empty Graph-yielding Dsimple Function;

coherence

for b_{1} being GraphSum of F holds b_{1} is Dsimple
;

end;
coherence

for b

registration

let F be non empty Graph-yielding edgeless Function;

coherence

for b_{1} being GraphSum of F holds b_{1} is edgeless
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds not b_{1} is edgeless
by Th124;

end;
coherence

for b

registration

let F be non empty Graph-yielding loopfull Function;

coherence

for b_{1} being GraphSum of F holds b_{1} is loopfull
by Th124;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds not b_{1} is loopfull
by Th124;

end;
coherence

for b

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

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;

coherence

for b_{1} being GraphSum of F holds b_{1} is acyclic
by Th125;

end;
coherence

for b

registration

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

coherence

for b_{1} being GraphSum of F holds not b_{1} is acyclic
by Th125;

end;
coherence

for b

theorem :: GLIB_015:126

for F being non empty Graph-yielding Function

for S being GraphSum of F holds card F c= S .numComponents()

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

for S being GraphSum of F holds card F = S .numComponents()

proof end;

definition

let G1, G2 be _Graph;

ex b_{1} being Supergraph of G1 st b_{1} is GraphSum of <*G1,G2*>

end;
mode GraphSum of G1,G2 -> Supergraph of G1 means :Def28: :: GLIB_015:def 28

it is GraphSum of <*G1,G2*>;

existence it is GraphSum of <*G1,G2*>;

ex b

proof end;

:: deftheorem Def28 defines GraphSum GLIB_015:def 28 :

for G1, G2 being _Graph

for b_{3} being Supergraph of G1 holds

( b_{3} is GraphSum of G1,G2 iff b_{3} is GraphSum of <*G1,G2*> );

for G1, G2 being _Graph

for b

( b

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

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;

coherence

for b_{1} being GraphSum of G1,G2 holds b_{1} is loopless
by Th128;

end;
coherence

for b

registration

let G1, G2 be non loopless _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds not b_{1} is loopless
;

end;
coherence

for b

registration

let G1, G2 be non-Dmulti _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds b_{1} is non-Dmulti
by Th128;

end;
coherence

for b

registration

let G1, G2 be non non-Dmulti _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds not b_{1} is non-Dmulti
;

end;
coherence

for b

registration

let G1, G2 be non-multi _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds b_{1} is non-multi
by Th128;

end;
coherence

for b

registration

let G1, G2 be non non-multi _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds not b_{1} is non-multi
;

end;
coherence

for b

registration
end;

registration
end;

registration

let G1, G2 be acyclic _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds b_{1} is acyclic
by Th128;

end;
coherence

for b

registration

let G1, G2 be non acyclic _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds not b_{1} is acyclic
;

end;
coherence

for b

registration

let G1, G2 be edgeless _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds b_{1} is edgeless
by Th128;

end;
coherence

for b

registration

let G1, G2 be non edgeless _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds not b_{1} is edgeless
;

end;
coherence

for b

registration

let G1, G2 be loopfull _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds b_{1} is loopfull
by Th128;

end;
coherence

for b

registration

let G1, G2 be non loopfull _Graph;

coherence

for b_{1} being GraphSum of G1,G2 holds not b_{1} is loopfull
by Th128;

end;
coherence

for b

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

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

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() = (G1 .numComponents()) +` (G2 .numComponents())

for S being GraphSum of G1,G2 holds S .numComponents() = (G1 .numComponents()) +` (G2 .numComponents())

proof end;