begin
:: deftheorem GLIB_000:def 1 :
canceled;
:: deftheorem defines VertexSelector GLIB_000:def 2 :
:: deftheorem defines EdgeSelector GLIB_000:def 3 :
:: deftheorem defines SourceSelector GLIB_000:def 4 :
:: deftheorem defines TargetSelector GLIB_000:def 5 :
:: deftheorem defines _GraphSelectors GLIB_000:def 6 :
:: deftheorem defines the_Vertices_of GLIB_000:def 7 :
:: deftheorem defines the_Edges_of GLIB_000:def 8 :
:: deftheorem defines the_Source_of GLIB_000:def 9 :
:: deftheorem defines the_Target_of GLIB_000:def 10 :
:: deftheorem Def11 defines [Graph-like] GLIB_000:def 11 :
definition
let V be non
empty set ;
let E be
set ;
let S,
T be
Function of
E,
V;
func createGraph V,
E,
S,
T -> _Graph equals
<*V,E,S,T*>;
coherence
<*V,E,S,T*> is _Graph
end;
:: deftheorem defines createGraph GLIB_000:def 12 :
:: deftheorem defines .set GLIB_000:def 13 :
:: deftheorem GLIB_000:def 14 :
canceled;
Lm1:
for GS being GraphStruct holds
( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) )
:: deftheorem Def15 defines Joins GLIB_000:def 15 :
:: deftheorem Def16 defines DJoins GLIB_000:def 16 :
:: deftheorem Def17 defines SJoins GLIB_000:def 17 :
:: deftheorem Def18 defines DSJoins GLIB_000:def 18 :
Lm2:
for G being _Graph
for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) )
definition
let G be
_Graph;
attr G is
finite means :
Def19:
(
the_Vertices_of G is
finite &
the_Edges_of G is
finite );
attr G is
loopless means :
Def20:
for
e being
set holds
( not
e in the_Edges_of G or not
(the_Source_of G) . e = (the_Target_of G) . e );
attr G is
trivial means :
Def21:
card (the_Vertices_of G) = 1;
attr G is
non-multi means :
Def22:
for
e1,
e2,
v1,
v2 being
set st
e1 Joins v1,
v2,
G &
e2 Joins v1,
v2,
G holds
e1 = e2;
attr G is
non-Dmulti means :
Def23:
for
e1,
e2,
v1,
v2 being
set st
e1 DJoins v1,
v2,
G &
e2 DJoins v1,
v2,
G holds
e1 = e2;
end;
:: deftheorem Def19 defines finite GLIB_000:def 19 :
:: deftheorem Def20 defines loopless GLIB_000:def 20 :
:: deftheorem Def21 defines trivial GLIB_000:def 21 :
:: deftheorem Def22 defines non-multi GLIB_000:def 22 :
:: deftheorem Def23 defines non-Dmulti GLIB_000:def 23 :
:: deftheorem Def24 defines simple GLIB_000:def 24 :
:: deftheorem Def25 defines Dsimple GLIB_000:def 25 :
Lm3:
for G being _Graph st the_Edges_of G = {} holds
G is simple
:: deftheorem defines .order() GLIB_000:def 26 :
:: deftheorem defines .size() GLIB_000:def 27 :
:: deftheorem Def28 defines .edgesInto GLIB_000:def 28 :
:: deftheorem Def29 defines .edgesOutOf GLIB_000:def 29 :
:: deftheorem defines .edgesInOut GLIB_000:def 30 :
:: deftheorem defines .edgesBetween GLIB_000:def 31 :
definition
let G be
_Graph;
let X,
Y be
set ;
func G .edgesBetween X,
Y -> Subset of
(the_Edges_of G) means :
Def32:
for
e being
set holds
(
e in it iff
e SJoins X,
Y,
G );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e SJoins X,Y,G )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e SJoins X,Y,G ) ) & ( for e being set holds
( e in b2 iff e SJoins X,Y,G ) ) holds
b1 = b2
func G .edgesDBetween X,
Y -> Subset of
(the_Edges_of G) means :
Def33:
for
e being
set holds
(
e in it iff
e DSJoins X,
Y,
G );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e DSJoins X,Y,G )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e DSJoins X,Y,G ) ) & ( for e being set holds
( e in b2 iff e DSJoins X,Y,G ) ) holds
b1 = b2
end;
:: deftheorem Def32 defines .edgesBetween GLIB_000:def 32 :
:: deftheorem Def33 defines .edgesDBetween GLIB_000:def 33 :
:: deftheorem Def34 defines Subgraph GLIB_000:def 34 :
Lm4:
for G being _Graph holds G is Subgraph of G
Lm5:
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
e Joins x,y,G1
:: deftheorem Def35 defines spanning GLIB_000:def 35 :
:: deftheorem Def36 defines == GLIB_000:def 36 :
:: deftheorem Def37 defines c= GLIB_000:def 37 :
:: deftheorem Def38 defines c< GLIB_000:def 38 :
for
G1,
G2 being
_Graph holds
(
G1 c< G2 iff (
G1 c= G2 &
G1 != G2 ) );
:: deftheorem Def39 defines inducedSubgraph GLIB_000:def 39 :
Lm6:
for G being _Graph
for e, X being set holds
( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X )
Lm7:
for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G)
:: deftheorem defines .edgesIn() GLIB_000:def 40 :
:: deftheorem defines .edgesOut() GLIB_000:def 41 :
:: deftheorem defines .edgesInOut() GLIB_000:def 42 :
Lm8:
for G being _Graph
for v being Vertex of G
for e being set holds
( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) )
Lm9:
for G being _Graph
for v being Vertex of G
for e being set holds
( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) )
:: deftheorem Def43 defines .adj GLIB_000:def 43 :
:: deftheorem defines .inDegree() GLIB_000:def 44 :
:: deftheorem defines .outDegree() GLIB_000:def 45 :
:: deftheorem defines .degree() GLIB_000:def 46 :
:: deftheorem defines .degree() GLIB_000:def 47 :
:: deftheorem defines .inNeighbors() GLIB_000:def 48 :
:: deftheorem defines .outNeighbors() GLIB_000:def 49 :
:: deftheorem defines .allNeighbors() GLIB_000:def 50 :
:: deftheorem Def51 defines isolated GLIB_000:def 51 :
:: deftheorem defines isolated GLIB_000:def 52 :
:: deftheorem Def53 defines endvertex GLIB_000:def 53 :
:: deftheorem defines endvertex GLIB_000:def 54 :
:: deftheorem Def55 defines Graph-yielding GLIB_000:def 55 :
:: deftheorem Def56 defines halting GLIB_000:def 56 :
:: deftheorem defines .Lifespan() GLIB_000:def 57 :
:: deftheorem defines .Result() GLIB_000:def 58 :
:: deftheorem GLIB_000:def 59 :
canceled;
:: deftheorem Def60 defines finite GLIB_000:def 60 :
:: deftheorem Def61 defines loopless GLIB_000:def 61 :
:: deftheorem Def62 defines trivial GLIB_000:def 62 :
:: deftheorem Def63 defines non-trivial GLIB_000:def 63 :
:: deftheorem Def64 defines non-multi GLIB_000:def 64 :
:: deftheorem Def65 defines non-Dmulti GLIB_000:def 65 :
:: deftheorem Def66 defines simple GLIB_000:def 66 :
:: deftheorem Def67 defines Dsimple GLIB_000:def 67 :
:: deftheorem defines halting GLIB_000:def 68 :
begin
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
for
V being non
empty set for
E being
set for
S,
T being
Function of
E,
V holds
(
the_Vertices_of (createGraph V,E,S,T) = V &
the_Edges_of (createGraph V,E,S,T) = E &
the_Source_of (createGraph V,E,S,T) = S &
the_Target_of (createGraph V,E,S,T) = T )
by FINSEQ_4:91;
theorem Th9:
theorem
canceled;
theorem Th11:
theorem Th12:
theorem
theorem
theorem
for
GS being
GraphStruct for
x,
y being
set for
n1,
n2 being
Nat st
n1 <> n2 holds
(
n1 in dom ((GS .set n1,x) .set n2,y) &
n2 in dom ((GS .set n1,x) .set n2,y) &
((GS .set n1,x) .set n2,y) . n1 = x &
((GS .set n1,x) .set n2,y) . n2 = y )
theorem
theorem
theorem
for
G being
_Graph for
e,
x1,
y1,
x2,
y2 being
set st
e Joins x1,
y1,
G &
e Joins x2,
y2,
G & not (
x1 = x2 &
y1 = y2 ) holds
(
x1 = y2 &
y1 = x2 )
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th25:
theorem
theorem
theorem
theorem
theorem
theorem Th31:
theorem
theorem
theorem
theorem
theorem
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem
theorem
theorem Th44:
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem
theorem Th52:
theorem
theorem Th54:
theorem
theorem Th56:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem
theorem
theorem
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
for
G1 being
_Graph for
G2 being
Subgraph of
G1 for
x,
y,
e being
set holds
( (
e Joins x,
y,
G2 implies
e Joins x,
y,
G1 ) & (
e DJoins x,
y,
G2 implies
e DJoins x,
y,
G1 ) & (
e SJoins x,
y,
G2 implies
e SJoins x,
y,
G1 ) & (
e DSJoins x,
y,
G2 implies
e DSJoins x,
y,
G1 ) )
theorem
for
G1 being
_Graph for
G2 being
Subgraph of
G1 for
x,
y,
e being
set st
e in the_Edges_of G2 holds
( (
e Joins x,
y,
G1 implies
e Joins x,
y,
G2 ) & (
e DJoins x,
y,
G1 implies
e DJoins x,
y,
G2 ) & (
e SJoins x,
y,
G1 implies
e SJoins x,
y,
G2 ) & (
e DSJoins x,
y,
G1 implies
e DSJoins x,
y,
G2 ) )
theorem
theorem
theorem
theorem
theorem Th81:
theorem Th82:
theorem
theorem
theorem
theorem
theorem
theorem Th88:
for
G1,
G2,
G3 being
_Graph st
G1 == G2 &
G2 == G3 holds
G1 == G3
theorem Th89:
theorem Th90:
theorem Th91:
for
G1,
G2 being
_Graph for
e,
x,
y,
X,
Y being
set st
G1 == G2 holds
( (
e Joins x,
y,
G1 implies
e Joins x,
y,
G2 ) & (
e DJoins x,
y,
G1 implies
e DJoins x,
y,
G2 ) & (
e SJoins X,
Y,
G1 implies
e SJoins X,
Y,
G2 ) & (
e DSJoins X,
Y,
G1 implies
e DSJoins X,
Y,
G2 ) )
theorem
theorem Th93:
theorem Th94:
theorem
theorem
theorem
theorem
theorem Th99:
theorem
theorem Th101:
theorem