:: by Sebastian Koch

::

:: Received June 29, 2018

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

definition

let G be _Graph;

let E be set ;

( ( E c= the_Edges_of G implies ex b_{1} being _Graph st

( the_Vertices_of b_{1} = the_Vertices_of G & the_Edges_of b_{1} = the_Edges_of G & the_Source_of b_{1} = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of b_{1} = (the_Target_of G) +* ((the_Source_of G) | E) ) ) & ( not E c= the_Edges_of G implies ex b_{1} being _Graph st b_{1} == G ) )

for b_{1} being _Graph holds verum
;

end;
let E be set ;

mode reverseEdgeDirections of G,E -> _Graph means :Def1: :: GLIB_007:def 1

( the_Vertices_of it = the_Vertices_of G & the_Edges_of it = the_Edges_of G & the_Source_of it = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of it = (the_Target_of G) +* ((the_Source_of G) | E) ) if E c= the_Edges_of G

otherwise it == G;

existence ( the_Vertices_of it = the_Vertices_of G & the_Edges_of it = the_Edges_of G & the_Source_of it = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of it = (the_Target_of G) +* ((the_Source_of G) | E) ) if E c= the_Edges_of G

otherwise it == G;

( ( E c= the_Edges_of G implies ex b

( the_Vertices_of b

proof end;

consistency for b

:: deftheorem Def1 defines reverseEdgeDirections GLIB_007:def 1 :

for G being _Graph

for E being set

for b_{3} being _Graph holds

( ( E c= the_Edges_of G implies ( b_{3} is reverseEdgeDirections of G,E iff ( the_Vertices_of b_{3} = the_Vertices_of G & the_Edges_of b_{3} = the_Edges_of G & the_Source_of b_{3} = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of b_{3} = (the_Target_of G) +* ((the_Source_of G) | E) ) ) ) & ( not E c= the_Edges_of G implies ( b_{3} is reverseEdgeDirections of G,E iff b_{3} == G ) ) );

for G being _Graph

for E being set

for b

( ( E c= the_Edges_of G implies ( b

definition
end;

theorem Th2: :: GLIB_007:2

for G, G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G,E st G1 == G2 holds

G2 is reverseEdgeDirections of G,E

for E being set

for G1 being reverseEdgeDirections of G,E st G1 == G2 holds

G2 is reverseEdgeDirections of G,E

proof end;

theorem Th3: :: GLIB_007:3

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E holds G2 is reverseEdgeDirections of G1,E

for E being set

for G1 being reverseEdgeDirections of G2,E holds G2 is reverseEdgeDirections of G1,E

proof end;

theorem Th4: :: GLIB_007:4

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E holds

( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

for E being set

for G1 being reverseEdgeDirections of G2,E holds

( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

proof end;

theorem Th5: :: GLIB_007:5

for G2 being _Graph

for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1

for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1

proof end;

theorem Th6: :: GLIB_007:6

for G2 being _trivial _Graph

for E being set

for G1 being _Graph holds

( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )

for E being set

for G1 being _Graph holds

( G1 == G2 iff G1 is reverseEdgeDirections of G2,E )

proof end;

Lm1: for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object st E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 holds

e DJoins v2,v1,G1

proof end;

theorem Th7: :: GLIB_007:7

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds

( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds

( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

proof end;

Lm2: for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E & e DJoins v1,v2,G2 holds

e DJoins v1,v2,G1

proof end;

theorem Th8: :: GLIB_007:8

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds

( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds

( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )

proof end;

Lm3: for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 holds

for v1, e, v2 being object st e Joins v1,v2,G2 holds

e Joins v1,v2,G1

proof end;

theorem Th9: :: GLIB_007:9

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object holds

( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, e, v2 being object holds

( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )

proof end;

theorem Th11: :: GLIB_007:11

for G2 being _Graph

for E, V being set

for G1 being reverseEdgeDirections of G2,E holds G1 .edgesBetween V = G2 .edgesBetween V

for E, V being set

for G1 being reverseEdgeDirections of G2,E holds G1 .edgesBetween V = G2 .edgesBetween V

proof end;

theorem Th12: :: GLIB_007:12

for G2 being _Graph

for E, V being set

for G1 being reverseEdgeDirections of G2,E holds G1 .edgesInOut V = G2 .edgesInOut V

for E, V being set

for G1 being reverseEdgeDirections of G2,E holds G1 .edgesInOut V = G2 .edgesInOut V

proof end;

theorem Th13: :: GLIB_007:13

for G2 being _Graph

for E, V being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

v1 .edgesInOut() = v2 .edgesInOut()

for E, V being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

v1 .edgesInOut() = v2 .edgesInOut()

proof end;

theorem Th14: :: GLIB_007:14

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2 holds W2 is Walk of G1

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2 holds W2 is Walk of G1

proof end;

theorem Th15: :: GLIB_007:15

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for W1 being Walk of G1 holds W1 is Walk of G2

for E being set

for G1 being reverseEdgeDirections of G2,E

for W1 being Walk of G1 holds W1 is Walk of G2

proof end;

theorem Th16: :: GLIB_007:16

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2

for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds

( W1 is directed iff W2 .reverse() is directed )

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2

for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds

( W1 is directed iff W2 .reverse() is directed )

proof end;

theorem :: GLIB_007:17

for G2 being _Graph

for G1 being reverseEdgeDirections of G2

for W2 being Walk of G2

for W1 being Walk of G1 st W1 = W2 holds

( W1 is directed iff W2 .reverse() is directed )

for G1 being reverseEdgeDirections of G2

for W2 being Walk of G2

for W1 being Walk of G1 st W1 = W2 holds

( W1 is directed iff W2 .reverse() is directed )

proof end;

Lm4: for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2

for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds

W2 is chordal

proof end;

theorem Th18: :: GLIB_007:18

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2

for W1 being Walk of G1 st W1 = W2 holds

( W1 is chordal iff W2 is chordal )

for E being set

for G1 being reverseEdgeDirections of G2,E

for W2 being Walk of G2

for W1 being Walk of G1 st W1 = W2 holds

( W1 is chordal iff W2 is chordal )

proof end;

theorem Th19: :: GLIB_007:19

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, v2 being object holds

( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1, v2 being object holds

( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )

proof end;

theorem Th20: :: GLIB_007:20

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

theorem Th21: :: GLIB_007:21

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E holds

( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )

for E being set

for G1 being reverseEdgeDirections of G2,E holds

( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )

proof end;

registration

let G be _trivial _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is _trivial

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non _trivial _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is _trivial

end;
let E be set ;

coherence

for b

proof end;

theorem Th22: :: GLIB_007:22

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v being set

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

for E being set

for G1 being reverseEdgeDirections of G2,E

for v being set

for G3 being removeVertex of G1,v

for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

proof end;

Lm5: for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )

proof end;

theorem :: GLIB_007:23

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )

for E being set

for G1 being reverseEdgeDirections of G2,E

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )

proof end;

theorem :: GLIB_007:24

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E holds

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

for E being set

for G1 being reverseEdgeDirections of G2,E holds

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

proof end;

theorem Th25: :: GLIB_007:25

for G2 being _Graph

for E being set

for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds

( not e1 in E & not e2 in E ) ) holds

G1 is non-Dmulti

for E being set

for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds

( not e1 in E & not e2 in E ) ) holds

G1 is non-Dmulti

proof end;

registration

let G be non-Dmulti _Graph;

coherence

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

end;
coherence

for b

proof end;

registration

let G be non non-Dmulti _Graph;

coherence

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

end;
coherence

for b

proof end;

registration

let G be non-multi _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is non-multi

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non non-multi _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is non-multi

end;
let E be set ;

coherence

for b

proof end;

registration

let G be loopless _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is loopless

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non loopless _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is loopless

end;
let E be set ;

coherence

for b

proof end;

registration

let G be connected _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is connected

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non connected _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is connected

end;
let E be set ;

coherence

for b

proof end;

registration

let G be acyclic _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is acyclic

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non acyclic _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is acyclic

end;
let E be set ;

coherence

for b

proof end;

registration

let G be complete _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is complete

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non complete _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is complete

end;
let E be set ;

coherence

for b

proof end;

registration

let G be chordal _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is chordal

end;
let E be set ;

coherence

for b

proof end;

:: "non"-version of this cluster has to wait

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

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

registration

let G be _finite _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is _finite

end;
let E be set ;

coherence

for b

proof end;

registration

let G be non _finite _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is _finite

end;
let E be set ;

coherence

for b

proof end;

theorem Th26: :: GLIB_007:26

for G2 being _Graph

for G1 being reverseEdgeDirections of G2 holds

( the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2 )

for G1 being reverseEdgeDirections of G2 holds

( the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2 )

proof end;

theorem :: GLIB_007:27

for G2 being _Graph

for G1 being reverseEdgeDirections of G2

for v1, e, v2 being object holds

( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

for G1 being reverseEdgeDirections of G2

for v1, e, v2 being object holds

( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

proof end;

Lm6: for X, Y being set holds X /\ (Y --> X) = {}

proof end;

Lm7: for X, Y being set

for x being object st X /\ Y = {} & x in X holds

not x in Y

by XBOOLE_0:def 4;

:: we need a lot of edges, so we take the freedom

:: to specify them within the definition

:: to specify them within the definition

definition

let G be _Graph;

let v be object ;

let V be set ;

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v} & the_Edges_of b_{1} = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b_{1} = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of b_{1} = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b_{1} being Supergraph of G st b_{1} == G ) )

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

end;
let v be object ;

let V be set ;

mode addAdjVertexToAll of G,v,V -> Supergraph of G means :Def2: :: GLIB_007:def 2

( the_Vertices_of it = (the_Vertices_of G) \/ {v} & the_Edges_of it = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of it = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of it = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )

otherwise it == G;

existence ( the_Vertices_of it = (the_Vertices_of G) \/ {v} & the_Edges_of it = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of it = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of it = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )

otherwise it == G;

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b

( the_Vertices_of b

proof end;

consistency for b

:: deftheorem Def2 defines addAdjVertexToAll GLIB_007:def 2 :

for G being _Graph

for v being object

for V being set

for b_{4} being Supergraph of G holds

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b_{4} is addAdjVertexToAll of G,v,V iff ( the_Vertices_of b_{4} = (the_Vertices_of G) \/ {v} & the_Edges_of b_{4} = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b_{4} = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of b_{4} = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b_{4} is addAdjVertexToAll of G,v,V iff b_{4} == G ) ) );

for G being _Graph

for v being object

for V being set

for b

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b

definition

let G be _Graph;

let v be object ;

let V be set ;

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v} & the_Edges_of b_{1} = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b_{1} = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of b_{1} = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b_{1} being Supergraph of G st b_{1} == G ) )

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

end;
let v be object ;

let V be set ;

mode addAdjVertexFromAll of G,v,V -> Supergraph of G means :Def3: :: GLIB_007:def 3

( the_Vertices_of it = (the_Vertices_of G) \/ {v} & the_Edges_of it = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of it = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of it = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )

otherwise it == G;

existence ( the_Vertices_of it = (the_Vertices_of G) \/ {v} & the_Edges_of it = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of it = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of it = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )

otherwise it == G;

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b

( the_Vertices_of b

proof end;

consistency for b

:: deftheorem Def3 defines addAdjVertexFromAll GLIB_007:def 3 :

for G being _Graph

for v being object

for V being set

for b_{4} being Supergraph of G holds

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b_{4} is addAdjVertexFromAll of G,v,V iff ( the_Vertices_of b_{4} = (the_Vertices_of G) \/ {v} & the_Edges_of b_{4} = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b_{4} = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of b_{4} = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b_{4} is addAdjVertexFromAll of G,v,V iff b_{4} == G ) ) );

for G being _Graph

for v being object

for V being set

for b

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b

definition

let G be _Graph;

let v be object ;

mode addAdjVertexToAll of G,v is addAdjVertexToAll of G,v, the_Vertices_of G;

correctness

;

mode addAdjVertexFromAll of G,v is addAdjVertexFromAll of G,v, the_Vertices_of G;

correctness

;

end;
let v be object ;

mode addAdjVertexToAll of G,v is addAdjVertexToAll of G,v, the_Vertices_of G;

correctness

;

mode addAdjVertexFromAll of G,v is addAdjVertexFromAll of G,v, the_Vertices_of G;

correctness

;

theorem :: GLIB_007:28

for G being _Graph

for v being object

for V being set

for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2

for v being object

for V being set

for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2

proof end;

theorem :: GLIB_007:29

for G being _Graph

for v being object

for V being set

for G1, G2 being addAdjVertexFromAll of G,v,V holds G1 == G2

for v being object

for V being set

for G1, G2 being addAdjVertexFromAll of G,v,V holds G1 == G2

proof end;

theorem :: GLIB_007:30

for G, G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds

G2 is addAdjVertexToAll of G,v,V

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds

G2 is addAdjVertexToAll of G,v,V

proof end;

theorem :: GLIB_007:31

for G, G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds

G2 is addAdjVertexFromAll of G,v,V

for v being object

for V being set

for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds

G2 is addAdjVertexFromAll of G,v,V

proof end;

theorem Th32: :: GLIB_007:32

for G being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V holds

( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V holds

( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

proof end;

theorem Th33: :: GLIB_007:33

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .edgesOutOf {v} = V --> (the_Edges_of G2)

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .edgesOutOf {v} = V --> (the_Edges_of G2)

proof end;

theorem Th34: :: GLIB_007:34

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .edgesInto {v} = V --> (the_Edges_of G2)

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .edgesInto {v} = V --> (the_Edges_of G2)

proof end;

theorem Th35: :: GLIB_007:35

for G being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds

( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds

( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )

proof end;

theorem :: GLIB_007:36

for G being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for v1, e, v2 being object holds

( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for v1, e, v2 being object holds

( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )

proof end;

theorem :: GLIB_007:37

for G being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for w being object holds

( w is Vertex of G1 iff w is Vertex of G2 ) by Th32;

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for w being object holds

( w is Vertex of G1 iff w is Vertex of G2 ) by Th32;

theorem Th38: :: GLIB_007:38

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e1, u being object holds

( not e1 DJoins u,v,G1 & ( not u in V implies not e1 DJoins v,u,G1 ) & ( for e2 being object st e1 DJoins v,u,G1 & e2 DJoins v,u,G1 holds

e1 = e2 ) )

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e1, u being object holds

( not e1 DJoins u,v,G1 & ( not u in V implies not e1 DJoins v,u,G1 ) & ( for e2 being object st e1 DJoins v,u,G1 & e2 DJoins v,u,G1 holds

e1 = e2 ) )

proof end;

theorem Th39: :: GLIB_007:39

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e1, u being object holds

( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds

e1 = e2 ) )

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e1, u being object holds

( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds

e1 = e2 ) )

proof end;

theorem Th40: :: GLIB_007:40

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds

e DJoins v1,v2,G2

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds

e DJoins v1,v2,G2

proof end;

theorem Th41: :: GLIB_007:41

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e, v1, v2 being object st v2 <> v & e DJoins v1,v2,G1 holds

e DJoins v1,v2,G2

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

for e, v1, v2 being object st v2 <> v & e DJoins v1,v2,G1 holds

e DJoins v1,v2,G2

proof end;

theorem Th42: :: GLIB_007:42

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V

for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds

[v1,(the_Edges_of G2)] DJoins v,v1,G1

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V

for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds

[v1,(the_Edges_of G2)] DJoins v,v1,G1

proof end;

theorem Th43: :: GLIB_007:43

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V

for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds

[v1,(the_Edges_of G2)] DJoins v1,v,G1

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V

for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds

[v1,(the_Edges_of G2)] DJoins v1,v,G1

proof end;

theorem :: GLIB_007:44

for G being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for W1 being Walk of G1 holds W1 is Walk of G2

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for W1 being Walk of G1 holds W1 is Walk of G2

proof end;

theorem :: GLIB_007:45

for G being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for W2 being Walk of G2 holds W2 is Walk of G1

for v being object

for V being set

for G1 being addAdjVertexToAll of G,v,V

for G2 being addAdjVertexFromAll of G,v,V

for W2 being Walk of G2 holds W2 is Walk of G1

proof end;

Lm8: for V, E being set holds card V = card (V --> E)

proof end;

Lm9: for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( ( for e being object holds

( not e Joins v,v,G1 & ( for v1 being object holds

( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds

e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds

ex e1 being object st

( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds

e1 = e2 ) ) ) ) )

proof end;

Lm10: for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( ( for e being object holds

( not e Joins v,v,G1 & ( for v1 being object holds

( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds

e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds

ex e1 being object st

( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds

e1 = e2 ) ) ) ) )

proof end;

:: If someone could come up with an easier redefinition

:: without using isomorphisms, it would be appreciated.

:: Note that each property of the definition is used within

:: the next three theorems.

:: Also note that about half the definition is implied when V is finite

:: because of the card-property. However, this will not be proved here.

:: We need this general form (as opposed to addAdjVertexTo/FromAll)

:: to give a constructive characterization of star and wheel graphs

:: without having to use isomorphisms.

:: without using isomorphisms, it would be appreciated.

:: Note that each property of the definition is used within

:: the next three theorems.

:: Also note that about half the definition is implied when V is finite

:: because of the card-property. However, this will not be proved here.

:: We need this general form (as opposed to addAdjVertexTo/FromAll)

:: to give a constructive characterization of star and wheel graphs

:: without having to use isomorphisms.

definition

let G be _Graph;

let v be object ;

let V be set ;

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = (the_Vertices_of G) \/ {v} & ( for e being object holds

( not e Joins v,v,b_{1} & ( for v1 being object holds

( ( not v1 in V implies not e Joins v1,v,b_{1} ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b_{1} holds

e DJoins v1,v2,G ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G & the_Edges_of b_{1} = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds

ex e1 being object st

( e1 in E & e1 Joins v1,v,b_{1} & ( for e2 being object st e2 Joins v1,v,b_{1} holds

e1 = e2 ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b_{1} being Supergraph of G st b_{1} == G ) )

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

end;
let v be object ;

let V be set ;

mode addAdjVertexAll of G,v,V -> Supergraph of G means :Def4: :: GLIB_007:def 4

( the_Vertices_of it = (the_Vertices_of G) \/ {v} & ( for e being object holds

( not e Joins v,v,it & ( for v1 being object holds

( ( not v1 in V implies not e Joins v1,v,it ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,it holds

e DJoins v1,v2,G ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G & the_Edges_of it = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds

ex e1 being object st

( e1 in E & e1 Joins v1,v,it & ( for e2 being object st e2 Joins v1,v,it holds

e1 = e2 ) ) ) ) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )

otherwise it == G;

existence ( the_Vertices_of it = (the_Vertices_of G) \/ {v} & ( for e being object holds

( not e Joins v,v,it & ( for v1 being object holds

( ( not v1 in V implies not e Joins v1,v,it ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,it holds

e DJoins v1,v2,G ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G & the_Edges_of it = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds

ex e1 being object st

( e1 in E & e1 Joins v1,v,it & ( for e2 being object st e2 Joins v1,v,it holds

e1 = e2 ) ) ) ) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )

otherwise it == G;

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b

( the_Vertices_of b

( not e Joins v,v,b

( ( not v1 in V implies not e Joins v1,v,b

e DJoins v1,v2,G ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G & the_Edges_of b

ex e1 being object st

( e1 in E & e1 Joins v1,v,b

e1 = e2 ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ex b

proof end;

consistency for b

:: deftheorem Def4 defines addAdjVertexAll GLIB_007:def 4 :

for G being _Graph

for v being object

for V being set

for b_{4} being Supergraph of G holds

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b_{4} is addAdjVertexAll of G,v,V iff ( the_Vertices_of b_{4} = (the_Vertices_of G) \/ {v} & ( for e being object holds

( not e Joins v,v,b_{4} & ( for v1 being object holds

( ( not v1 in V implies not e Joins v1,v,b_{4} ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b_{4} holds

e DJoins v1,v2,G ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G & the_Edges_of b_{4} = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds

ex e1 being object st

( e1 in E & e1 Joins v1,v,b_{4} & ( for e2 being object st e2 Joins v1,v,b_{4} holds

e1 = e2 ) ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b_{4} is addAdjVertexAll of G,v,V iff b_{4} == G ) ) );

for G being _Graph

for v being object

for V being set

for b

( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b

( not e Joins v,v,b

( ( not v1 in V implies not e Joins v1,v,b

e DJoins v1,v2,G ) ) ) ) ) & ex E being set st

( card V = card E & E misses the_Edges_of G & the_Edges_of b

ex e1 being object st

( e1 in E & e1 Joins v1,v,b

e1 = e2 ) ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b

definition

let G be _Graph;

let v be object ;

mode addAdjVertexAll of G,v is addAdjVertexAll of G,v, the_Vertices_of G;

correctness

;

let V be set ;

:: original: addAdjVertexToAll

redefine mode addAdjVertexToAll of G,v,V -> addAdjVertexAll of G,v,V;

coherence

for b_{1} being addAdjVertexToAll of G,v,V holds b_{1} is addAdjVertexAll of G,v,V

redefine mode addAdjVertexFromAll of G,v,V -> addAdjVertexAll of G,v,V;

coherence

for b_{1} being addAdjVertexFromAll of G,v,V holds b_{1} is addAdjVertexAll of G,v,V

end;
let v be object ;

mode addAdjVertexAll of G,v is addAdjVertexAll of G,v, the_Vertices_of G;

correctness

;

let V be set ;

:: original: addAdjVertexToAll

redefine mode addAdjVertexToAll of G,v,V -> addAdjVertexAll of G,v,V;

coherence

for b

proof end;

:: original: addAdjVertexFromAllredefine mode addAdjVertexFromAll of G,v,V -> addAdjVertexAll of G,v,V;

coherence

for b

proof end;

theorem Th46: :: GLIB_007:46

for G2 being _Graph

for v being object

for G1 being addAdjVertexAll of G2,v, {} holds the_Edges_of G2 = the_Edges_of G1

for v being object

for G1 being addAdjVertexAll of G2,v, {} holds the_Edges_of G2 = the_Edges_of G1

proof end;

Lm11: for G2 being _Graph

for v being object

for G1 being addAdjVertexAll of G2,v, {} st the_Edges_of G2 = {} holds

the_Edges_of G1 = {}

by Th46;

theorem Th47: :: GLIB_007:47

for G2 being _Graph

for v being object

for V being non empty set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

the_Edges_of G1 <> {}

for v being object

for V being non empty set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

the_Edges_of G1 <> {}

proof end;

theorem :: GLIB_007:48

for G, G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G,v,V st G1 == G2 holds

G2 is addAdjVertexAll of G,v,V

for v being object

for V being set

for G1 being addAdjVertexAll of G,v,V st G1 == G2 holds

G2 is addAdjVertexAll of G,v,V

proof end;

theorem Th49: :: GLIB_007:49

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds

e Joins v1,v2,G2

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds

e Joins v1,v2,G2

proof end;

theorem Th50: :: GLIB_007:50

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

v is Vertex of G1

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

v is Vertex of G1

proof end;

theorem Th51: :: GLIB_007:51

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for E being set

for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds

( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for E being set

for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds

( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

proof end;

theorem Th52: :: GLIB_007:52

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds

ex f, g being Function of E,(V \/ {v}) st

( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds

( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds

ex f, g being Function of E,(V \/ {v}) st

( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds

( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )

proof end;

theorem Th53: :: GLIB_007:53

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)

proof end;

theorem :: GLIB_007:54

for G2 being _Graph

for v, V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G2 is removeVertex of G1,v

for v, V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G2 is removeVertex of G1,v

proof end;

theorem Th55: :: GLIB_007:55

for G2 being _Graph

for v being object

for G1 being addAdjVertexAll of G2,v, {} holds G1 is addVertex of G2,v

for v being object

for G1 being addAdjVertexAll of G2,v, {} holds G1 is addVertex of G2,v

proof end;

:: TODO other direction

theorem :: GLIB_007:56

for G2 being _Graph

for v, v1 being object

for G1 being addAdjVertexAll of G2,v,{v1} st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 holds

ex e being object st

( not e in the_Edges_of G2 & ( G1 is addAdjVertex of G2,v,e,v1 or G1 is addAdjVertex of G2,v1,e,v ) )

for v, v1 being object

for G1 being addAdjVertexAll of G2,v,{v1} st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 holds

ex e being object st

( not e in the_Edges_of G2 & ( G1 is addAdjVertex of G2,v,e,v1 or G1 is addAdjVertex of G2,v1,e,v ) )

proof end;

Lm12: for G2 being _Graph

for v being object

for V being set

for W being Subset of V

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds

W = {}

proof end;

theorem Th57: :: GLIB_007:57

for G2 being _Graph

for v being object

for V being set

for W being Subset of V

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

ex f being Function of W,(G1 .edgesBetween (W,{v})) st

( f is one-to-one & f is onto & ( for w being object st w in W holds

f . w Joins w,v,G1 ) )

for v being object

for V being set

for W being Subset of V

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

ex f being Function of W,(G1 .edgesBetween (W,{v})) st

( f is one-to-one & f is onto & ( for w being object st w in W holds

f . w Joins w,v,G1 ) )

proof end;

theorem Th58: :: GLIB_007:58

for G2 being _Graph

for v being object

for V, E being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds

E = G1 .edgesBetween (V,{v})

for v being object

for V, E being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds

E = G1 .edgesBetween (V,{v})

proof end;

theorem :: GLIB_007:59

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )

proof end;

theorem Th60: :: GLIB_007:60

for G3 being _Graph

for v being object

for V1, V2 being set

for G1 being addAdjVertexAll of G3,v,V1 \/ V2

for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds

G2 is addAdjVertexAll of G3,v,V1

for v being object

for V1, V2 being set

for G1 being addAdjVertexAll of G3,v,V1 \/ V2

for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds

G2 is addAdjVertexAll of G3,v,V1

proof end;

theorem :: GLIB_007:61

for G3 being _Graph

for v being object

for V being set

for v1 being Vertex of G3

for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds

ex G2 being addAdjVertexAll of G3,v,V ex e being object st

( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )

for v being object

for V being set

for v1 being Vertex of G3

for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds

ex G2 being addAdjVertexAll of G3,v,V ex e being object st

( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )

proof end;

theorem :: GLIB_007:62

for G3 being _Graph

for v being object

for V being set

for v1 being Vertex of G3

for e being object

for G2 being addAdjVertexAll of G3,v,V st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V & not e in the_Edges_of G2 holds

for G1 being _Graph st ( G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1 ) holds

G1 is addAdjVertexAll of G3,v,V \/ {v1}

for v being object

for V being set

for v1 being Vertex of G3

for e being object

for G2 being addAdjVertexAll of G3,v,V st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V & not e in the_Edges_of G2 holds

for G1 being _Graph st ( G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1 ) holds

G1 is addAdjVertexAll of G3,v,V \/ {v1}

proof end;

Lm13: for k being odd Element of NAT st 1 < k holds

k - 2 is odd Element of NAT

proof end;

theorem Th63: :: GLIB_007:63

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )

proof end;

theorem Th64: :: GLIB_007:64

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is V5() ) or not v in W .vertices() ) holds

W is Walk of G2

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is V5() ) or not v in W .vertices() ) holds

W is Walk of G2

proof end;

theorem Th65: :: GLIB_007:65

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds

W .edges() c= the_Edges_of G2

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds

W .edges() c= the_Edges_of G2

proof end;

theorem :: GLIB_007:66

for G being _Graph

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V holds

( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V holds

( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )

proof end;

theorem Th67: :: GLIB_007:67

for G being _Graph

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V

for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds

ex e2 being object st e2 Joins v1,v2,G2

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V

for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds

ex e2 being object st e2 Joins v1,v2,G2

proof end;

:: The closest analogon we can get for

:: theorem for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V

:: holds G1 == G2

:: but also preparation for

:: registration let G, v, V; let G1 being addAdjVertexAll of G,v,V;

:: cluster -> G1-isomorphic for addAdjVertexAll of G,v,V;

:: coming soon

:: theorem for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V

:: holds G1 == G2

:: but also preparation for

:: registration let G, v, V; let G1 being addAdjVertexAll of G,v,V;

:: cluster -> G1-isomorphic for addAdjVertexAll of G,v,V;

:: coming soon

theorem :: GLIB_007:68

for G being _Graph

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st

( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds

f . e Joins v1,v2,G2 ) )

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st

( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds

f . e Joins v1,v2,G2 ) )

proof end;

registration

let G be loopless _Graph;

let v be object ;

let V be set ;

coherence

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

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be non-Dmulti _Graph;

let v be object ;

let V be set ;

coherence

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

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be non-multi _Graph;

let v be object ;

let V be set ;

coherence

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

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be Dsimple _Graph;

let v be object ;

let V be set ;

coherence

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

end;
let v be object ;

let V be set ;

coherence

for b

registration

let G be simple _Graph;

let v be object ;

let V be set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is simple
;

end;
let v be object ;

let V be set ;

coherence

for b

theorem Th69: :: GLIB_007:69

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1

for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds

v in W .vertices()

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V

for W being Walk of G1

for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds

v in W .vertices()

proof end;

Lm14: for k being odd Element of NAT holds

( (k -' 1) + 1 = k & ( for n being Element of NAT st k <= n holds

k -' 1 < n ) )

proof end;

Lm15: for k, n being odd Element of NAT holds n + (k -' 1) is odd Element of NAT

proof end;

Lm16: ( 1 is odd Element of NAT & 3 is odd Element of NAT )

by POLYFORM:4, POLYFORM:6;

:: this means that in each component there is at most one

:: vertex connecting to the new one

:: vertex connecting to the new one

theorem :: GLIB_007:70

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2

for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds

w1 = w2 ) holds

G1 is acyclic

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2

for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds

w1 = w2 ) holds

G1 is acyclic

proof end;

theorem :: GLIB_007:71

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( not G2 is acyclic or ex G3 being Component of G2 ex w1, w2 being Vertex of G3 st

( w1 in V & w2 in V & w1 <> w2 ) ) holds

not G1 is acyclic

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( not G2 is acyclic or ex G3 being Component of G2 ex w1, w2 being Vertex of G3 st

( w1 in V & w2 in V & w1 <> w2 ) ) holds

not G1 is acyclic

proof end;

:: this means that in each component there is at least one

:: vertex connecting to the new one

:: vertex connecting to the new one

theorem Th72: :: GLIB_007:72

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( for G3 being Component of G2 ex w being Vertex of G3 st w in V ) holds

G1 is connected

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( for G3 being Component of G2 ex w being Vertex of G3 st w in V ) holds

G1 is connected

proof end;

registration

let G be connected _Graph;

let v be object ;

let V be non empty set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is connected

end;
let v be object ;

let V be non empty set ;

coherence

for b

proof end;

theorem Th73: :: GLIB_007:73

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st

for w being Vertex of G3 holds not w in V holds

not G1 is connected

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st

for w being Vertex of G3 holds not w in V holds

not G1 is connected

proof end;

theorem :: GLIB_007:74

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds

not G1 is connected

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds

not G1 is connected

proof end;

registration

let G be non connected _Graph;

let v be object ;

coherence

for b_{1} being addAdjVertexAll of G,v, {} holds not b_{1} is connected

end;
let v be object ;

coherence

for b

proof end;

theorem Th75: :: GLIB_007:75

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )

proof end;

registration

let G be complete _Graph;

coherence

for b_{1} being addAdjVertexAll of G, the_Vertices_of G holds b_{1} is complete

end;
coherence

for b

proof end;

theorem :: GLIB_007:76

for G2 being _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( G1 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) )

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

( G1 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) )

proof end;

theorem :: GLIB_007:77

for G2 being _finite _Graph

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .order() = (G2 .order()) + 1

for v being object

for V being set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .order() = (G2 .order()) + 1

proof end;

theorem :: GLIB_007:78

for G2 being _finite _Graph

for v being object

for V being finite set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .size() = (G2 .size()) + (card V)

for v being object

for V being finite set

for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds

G1 .size() = (G2 .size()) + (card V)

proof end;

registration

let G be _finite _Graph;

let v be object ;

let V be set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is _finite

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

:: subgraph modes. This particular example was needed

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

:: with (partially) reversed edge directions