begin
:: deftheorem GLIB_000:def 1 :
canceled;
:: deftheorem defines VertexSelector GLIB_000:def 2 :
VertexSelector = 1;
:: deftheorem defines EdgeSelector GLIB_000:def 3 :
EdgeSelector = 2;
:: deftheorem defines SourceSelector GLIB_000:def 4 :
SourceSelector = 3;
:: deftheorem defines TargetSelector GLIB_000:def 5 :
TargetSelector = 4;
:: deftheorem defines _GraphSelectors GLIB_000:def 6 :
_GraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector};
:: deftheorem defines the_Vertices_of GLIB_000:def 7 :
for G being GraphStruct holds the_Vertices_of G = G . VertexSelector;
:: deftheorem defines the_Edges_of GLIB_000:def 8 :
for G being GraphStruct holds the_Edges_of G = G . EdgeSelector;
:: deftheorem defines the_Source_of GLIB_000:def 9 :
for G being GraphStruct holds the_Source_of G = G . SourceSelector;
:: deftheorem defines the_Target_of GLIB_000:def 10 :
for G being GraphStruct holds the_Target_of G = G . TargetSelector;
:: deftheorem Def11 defines [Graph-like] GLIB_000:def 11 :
for G being GraphStruct holds
( G is [Graph-like] iff ( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & the_Vertices_of G is non empty set & the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) & the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) ) );
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 :
for V being non empty set
for E being set
for S, T being Function of E,V holds createGraph (V,E,S,T) = <*V,E,S,T*>;
:: deftheorem defines .set GLIB_000:def 13 :
for G being GraphStruct
for n being Nat
for x being set holds G .set (n,x) = G +* (n .--> x);
:: 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 :
for G being _Graph
for x, y, e being set holds
( e Joins x,y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) ) );
:: deftheorem Def16 defines DJoins GLIB_000:def 16 :
for G being _Graph
for x, y, e being set holds
( e DJoins x,y,G iff ( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y ) );
:: deftheorem Def17 defines SJoins GLIB_000:def 17 :
for G being _Graph
for X, Y, e being set holds
( e SJoins X,Y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y & (the_Target_of G) . e in X ) ) ) );
:: deftheorem Def18 defines DSJoins GLIB_000:def 18 :
for G being _Graph
for X, Y, e being set holds
( e DSJoins X,Y,G iff ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) );
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 :
for G being _Graph holds
( G is finite iff ( the_Vertices_of G is finite & the_Edges_of G is finite ) );
:: deftheorem Def20 defines loopless GLIB_000:def 20 :
for G being _Graph holds
( G is loopless iff for e being set holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) );
:: deftheorem Def21 defines trivial GLIB_000:def 21 :
for G being _Graph holds
( G is trivial iff card (the_Vertices_of G) = 1 );
:: deftheorem Def22 defines non-multi GLIB_000:def 22 :
for G being _Graph holds
( G is non-multi iff for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2 );
:: deftheorem Def23 defines non-Dmulti GLIB_000:def 23 :
for G being _Graph holds
( G is non-Dmulti iff for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2 );
:: deftheorem Def24 defines simple GLIB_000:def 24 :
for G being _Graph holds
( G is simple iff ( G is loopless & G is non-multi ) );
:: deftheorem Def25 defines Dsimple GLIB_000:def 25 :
for G being _Graph holds
( G is Dsimple iff ( G is loopless & G is non-Dmulti ) );
Lm3:
for G being _Graph st the_Edges_of G = {} holds
G is simple
:: deftheorem defines .order() GLIB_000:def 26 :
for G being _Graph holds G .order() = card (the_Vertices_of G);
:: deftheorem defines .size() GLIB_000:def 27 :
for G being _Graph holds G .size() = card (the_Edges_of G);
:: deftheorem Def28 defines .edgesInto GLIB_000:def 28 :
for G being _Graph
for X being set
for b3 being Subset of (the_Edges_of G) holds
( b3 = G .edgesInto X iff for e being set holds
( e in b3 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) );
:: deftheorem Def29 defines .edgesOutOf GLIB_000:def 29 :
for G being _Graph
for X being set
for b3 being Subset of (the_Edges_of G) holds
( b3 = G .edgesOutOf X iff for e being set holds
( e in b3 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) );
:: deftheorem defines .edgesInOut GLIB_000:def 30 :
for G being _Graph
for X being set holds G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X);
:: deftheorem defines .edgesBetween GLIB_000:def 31 :
for G being _Graph
for X being set holds G .edgesBetween X = (G .edgesInto X) /\ (G .edgesOutOf X);
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 :
for G being _Graph
for X, Y being set
for b4 being Subset of (the_Edges_of G) holds
( b4 = G .edgesBetween (X,Y) iff for e being set holds
( e in b4 iff e SJoins X,Y,G ) );
:: deftheorem Def33 defines .edgesDBetween GLIB_000:def 33 :
for G being _Graph
for X, Y being set
for b4 being Subset of (the_Edges_of G) holds
( b4 = G .edgesDBetween (X,Y) iff for e being set holds
( e in b4 iff e DSJoins X,Y,G ) );
:: deftheorem Def34 defines Subgraph GLIB_000:def 34 :
for G, b2 being _Graph holds
( b2 is Subgraph of G iff ( the_Vertices_of b2 c= the_Vertices_of G & the_Edges_of b2 c= the_Edges_of G & ( for e being set st e in the_Edges_of b2 holds
( (the_Source_of b2) . e = (the_Source_of G) . e & (the_Target_of b2) . e = (the_Target_of G) . e ) ) ) );
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 :
for G1 being _Graph
for G2 being Subgraph of G1 holds
( G2 is spanning iff the_Vertices_of G2 = the_Vertices_of G1 );
:: deftheorem Def36 defines == GLIB_000:def 36 :
for G1, G2 being _Graph holds
( G1 == G2 iff ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) );
:: deftheorem Def37 defines c= GLIB_000:def 37 :
for G1, G2 being _Graph holds
( G1 c= G2 iff G1 is Subgraph of G2 );
:: 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 :
for G being _Graph
for V, E being set
for b4 being Subgraph of G holds
( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ( b4 is inducedSubgraph of G,V,E iff ( the_Vertices_of b4 = V & the_Edges_of b4 = E ) ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ( b4 is inducedSubgraph of G,V,E iff b4 == G ) ) );
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 :
for G being _Graph
for v being Vertex of G holds v .edgesIn() = G .edgesInto {v};
:: deftheorem defines .edgesOut() GLIB_000:def 41 :
for G being _Graph
for v being Vertex of G holds v .edgesOut() = G .edgesOutOf {v};
:: deftheorem defines .edgesInOut() GLIB_000:def 42 :
for G being _Graph
for v being Vertex of G holds v .edgesInOut() = G .edgesInOut {v};
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 :
for G being _Graph
for v being Vertex of G
for e being set holds
( ( e in the_Edges_of G & (the_Target_of G) . e = v implies v .adj e = (the_Source_of G) . e ) & ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v implies v .adj e = (the_Target_of G) . e ) & ( ( not e in the_Edges_of G or not (the_Target_of G) . e = v ) & ( not e in the_Edges_of G or not (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies v .adj e = v ) );
:: deftheorem defines .inDegree() GLIB_000:def 44 :
for G being _Graph
for v being Vertex of G holds v .inDegree() = card (v .edgesIn());
:: deftheorem defines .outDegree() GLIB_000:def 45 :
for G being _Graph
for v being Vertex of G holds v .outDegree() = card (v .edgesOut());
:: deftheorem defines .degree() GLIB_000:def 46 :
for G being _Graph
for v being Vertex of G holds v .degree() = (v .inDegree()) +` (v .outDegree());
:: deftheorem defines .degree() GLIB_000:def 47 :
for G being finite _Graph
for v being Vertex of G holds v .degree() = (v .inDegree()) + (v .outDegree());
:: deftheorem defines .inNeighbors() GLIB_000:def 48 :
for G being _Graph
for v being Vertex of G holds v .inNeighbors() = (the_Source_of G) .: (v .edgesIn());
:: deftheorem defines .outNeighbors() GLIB_000:def 49 :
for G being _Graph
for v being Vertex of G holds v .outNeighbors() = (the_Target_of G) .: (v .edgesOut());
:: deftheorem defines .allNeighbors() GLIB_000:def 50 :
for G being _Graph
for v being Vertex of G holds v .allNeighbors() = (v .inNeighbors()) \/ (v .outNeighbors());
:: deftheorem Def51 defines isolated GLIB_000:def 51 :
for G being _Graph
for v being Vertex of G holds
( v is isolated iff v .edgesInOut() = {} );
:: deftheorem defines isolated GLIB_000:def 52 :
for G being finite _Graph
for v being Vertex of G holds
( v is isolated iff v .degree() = 0 );
:: deftheorem Def53 defines endvertex GLIB_000:def 53 :
for G being _Graph
for v being Vertex of G holds
( v is endvertex iff ex e being set st
( v .edgesInOut() = {e} & not e Joins v,v,G ) );
:: deftheorem defines endvertex GLIB_000:def 54 :
for G being finite _Graph
for v being Vertex of G holds
( v is endvertex iff v .degree() = 1 );
:: deftheorem Def55 defines Graph-yielding GLIB_000:def 55 :
for F being ManySortedSet of NAT holds
( F is Graph-yielding iff for n being Nat holds F . n is _Graph );
:: deftheorem Def56 defines halting GLIB_000:def 56 :
for F being ManySortedSet of NAT holds
( F is halting iff ex n being Nat st F . n = F . (n + 1) );
:: deftheorem defines .Lifespan() GLIB_000:def 57 :
for F being ManySortedSet of NAT
for b2 being Element of NAT holds
( ( F is halting implies ( b2 = F .Lifespan() iff ( F . b2 = F . (b2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b2 <= n ) ) ) ) & ( not F is halting implies ( b2 = F .Lifespan() iff b2 = 0 ) ) );
:: deftheorem defines .Result() GLIB_000:def 58 :
for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan());
:: deftheorem GLIB_000:def 59 :
canceled;
:: deftheorem Def60 defines finite GLIB_000:def 60 :
for GSq being GraphSeq holds
( GSq is finite iff for x being Nat holds GSq . x is finite );
:: deftheorem Def61 defines loopless GLIB_000:def 61 :
for GSq being GraphSeq holds
( GSq is loopless iff for x being Nat holds GSq . x is loopless );
:: deftheorem Def62 defines trivial GLIB_000:def 62 :
for GSq being GraphSeq holds
( GSq is trivial iff for x being Nat holds GSq . x is trivial );
:: deftheorem Def63 defines non-trivial GLIB_000:def 63 :
for GSq being GraphSeq holds
( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial );
:: deftheorem Def64 defines non-multi GLIB_000:def 64 :
for GSq being GraphSeq holds
( GSq is non-multi iff for x being Nat holds GSq . x is non-multi );
:: deftheorem Def65 defines non-Dmulti GLIB_000:def 65 :
for GSq being GraphSeq holds
( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti );
:: deftheorem Def66 defines simple GLIB_000:def 66 :
for GSq being GraphSeq holds
( GSq is simple iff for x being Nat holds GSq . x is simple );
:: deftheorem Def67 defines Dsimple GLIB_000:def 67 :
for GSq being GraphSeq holds
( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple );
:: deftheorem defines halting GLIB_000:def 68 :
for GSq being GraphSeq holds
( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) );
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