:: by Gilbert Lee and Piotr Rudnicki

::

:: Received February 22, 2005

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

registration
end;

definition

coherence

1 is Element of NAT ;

coherence

2 is Element of NAT ;

coherence

3 is Element of NAT ;

coherence

4 is Element of NAT ;

end;
1 is Element of NAT ;

coherence

2 is Element of NAT ;

coherence

3 is Element of NAT ;

coherence

4 is Element of NAT ;

definition

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty Subset of NAT ;

end;

func _GraphSelectors -> non empty Subset of NAT equals :: GLIB_000:def 5

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

coherence {VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty Subset of NAT ;

:: deftheorem defines _GraphSelectors GLIB_000:def 5 :

_GraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

_GraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

definition

let G be GraphStruct;

coherence

G . VertexSelector is set ;

coherence

G . EdgeSelector is set ;

coherence

G . SourceSelector is set ;

coherence

G . TargetSelector is set ;

end;
coherence

G . VertexSelector is set ;

coherence

G . EdgeSelector is set ;

coherence

G . SourceSelector is set ;

coherence

G . TargetSelector is set ;

:: deftheorem defines the_Vertices_of GLIB_000:def 6 :

for G being GraphStruct holds the_Vertices_of G = G . VertexSelector;

for G being GraphStruct holds the_Vertices_of G = G . VertexSelector;

:: deftheorem defines the_Edges_of GLIB_000:def 7 :

for G being GraphStruct holds the_Edges_of G = G . EdgeSelector;

for G being GraphStruct holds the_Edges_of G = G . EdgeSelector;

:: deftheorem defines the_Source_of GLIB_000:def 8 :

for G being GraphStruct holds the_Source_of G = G . SourceSelector;

for G being GraphStruct holds the_Source_of G = G . SourceSelector;

:: deftheorem defines the_Target_of GLIB_000:def 9 :

for G being GraphStruct holds the_Target_of G = G . TargetSelector;

for G being GraphStruct holds the_Target_of G = G . TargetSelector;

definition

let G be GraphStruct;

end;
attr G is [Graph-like] means :Def10: :: GLIB_000:def 10

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

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

:: deftheorem Def10 defines [Graph-like] GLIB_000:def 10 :

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

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 G be _Graph;

:: original: the_Source_of

redefine func the_Source_of G -> Function of (the_Edges_of G),(the_Vertices_of G);

coherence

the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10;

:: original: the_Target_of

redefine func the_Target_of G -> Function of (the_Edges_of G),(the_Vertices_of G);

coherence

the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10;

end;
:: original: the_Source_of

redefine func the_Source_of G -> Function of (the_Edges_of G),(the_Vertices_of G);

coherence

the_Source_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10;

:: original: the_Target_of

redefine func the_Target_of G -> Function of (the_Edges_of G),(the_Vertices_of G);

coherence

the_Target_of G is Function of (the_Edges_of G),(the_Vertices_of G) by Def10;

definition

let V be non empty set ;

let E be set ;

let S, T be Function of E,V;

coherence

<*V,E,S,T*> is _Graph

end;
let E be set ;

let S, T be Function of E,V;

coherence

<*V,E,S,T*> is _Graph

proof end;

:: deftheorem defines createGraph GLIB_000:def 11 :

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

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

definition

let G be GraphStruct;

let n be Nat;

let x be set ;

coherence

G +* (n .--> x) is GraphStruct

end;
let n be Nat;

let x be set ;

coherence

G +* (n .--> x) is GraphStruct

proof end;

:: deftheorem defines .set GLIB_000:def 12 :

for G being GraphStruct

for n being Nat

for x being set holds G .set (n,x) = G +* (n .--> x);

for G being GraphStruct

for n being Nat

for x being set holds G .set (n,x) = G +* (n .--> x);

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

proof end;

definition

let G be _Graph;

let x, y, e be object ;

end;
let x, y, e be object ;

pred e Joins x,y,G means :: GLIB_000:def 13

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

( 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 defines Joins GLIB_000:def 13 :

for G being _Graph

for x, y, e being object 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 ) ) ) );

for G being _Graph

for x, y, e being object 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 ) ) ) );

definition

let G be _Graph;

let x, y, e be object ;

end;
let x, y, e be object ;

pred e DJoins x,y,G means :: GLIB_000:def 14

( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y );

( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y );

:: deftheorem defines DJoins GLIB_000:def 14 :

for G being _Graph

for x, y, e being object 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 ) );

for G being _Graph

for x, y, e being object 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 ) );

definition

let G be _Graph;

let X, Y be set ;

let e be object ;

end;
let X, Y be set ;

let e be object ;

pred e SJoins X,Y,G means :: GLIB_000:def 15

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

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

pred e DSJoins X,Y,G means :: GLIB_000:def 16

( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y );

( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y );

:: deftheorem defines SJoins GLIB_000:def 15 :

for G being _Graph

for X, Y being set

for e being object 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 ) ) ) );

for G being _Graph

for X, Y being set

for e being object 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 defines DSJoins GLIB_000:def 16 :

for G being _Graph

for X, Y being set

for e being object 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 ) );

for G being _Graph

for X, Y being set

for e being object 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 ) );

definition

let G be _Graph;

end;
attr G is finite means :Def17: :: GLIB_000:def 17

( the_Vertices_of G is finite & the_Edges_of G is finite );

( the_Vertices_of G is finite & the_Edges_of G is finite );

attr G is loopless means :Def18: :: GLIB_000:def 18

for e being object holds

( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e );

for e being object holds

( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e );

attr G is non-multi means :Def20: :: GLIB_000:def 20

for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds

e1 = e2;

for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds

e1 = e2;

attr G is non-Dmulti means :: GLIB_000:def 21

for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds

e1 = e2;

for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds

e1 = e2;

:: deftheorem Def17 defines finite GLIB_000:def 17 :

for G being _Graph holds

( G is finite iff ( the_Vertices_of G is finite & the_Edges_of G is finite ) );

for G being _Graph holds

( G is finite iff ( the_Vertices_of G is finite & the_Edges_of G is finite ) );

:: deftheorem Def18 defines loopless GLIB_000:def 18 :

for G being _Graph holds

( G is loopless iff for e being object holds

( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) );

for G being _Graph holds

( G is loopless iff for e being object holds

( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) );

:: deftheorem Def19 defines trivial GLIB_000:def 19 :

for G being _Graph holds

( G is trivial iff card (the_Vertices_of G) = 1 );

for G being _Graph holds

( G is trivial iff card (the_Vertices_of G) = 1 );

:: deftheorem Def20 defines non-multi GLIB_000:def 20 :

for G being _Graph holds

( G is non-multi iff for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds

e1 = e2 );

for G being _Graph holds

( G is non-multi iff for e1, e2, v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds

e1 = e2 );

:: deftheorem defines non-Dmulti GLIB_000:def 21 :

for G being _Graph holds

( G is non-Dmulti iff for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds

e1 = e2 );

for G being _Graph holds

( G is non-Dmulti iff for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds

e1 = e2 );

:: deftheorem defines simple GLIB_000:def 22 :

for G being _Graph holds

( G is simple iff ( G is loopless & G is non-multi ) );

for G being _Graph holds

( G is simple iff ( G is loopless & G is non-multi ) );

:: deftheorem defines Dsimple GLIB_000:def 23 :

for G being _Graph holds

( G is Dsimple iff ( G is loopless & G is non-Dmulti ) );

for G being _Graph holds

( G is Dsimple iff ( G is loopless & G is non-Dmulti ) );

Lm2: for G being _Graph st the_Edges_of G = {} holds

G is simple

proof end;

registration

for b_{1} being _Graph st b_{1} is non-multi holds

b_{1} is non-Dmulti

for b_{1} being _Graph st b_{1} is simple holds

( b_{1} is loopless & b_{1} is non-multi )
;

for b_{1} being _Graph st b_{1} is loopless & b_{1} is non-multi holds

b_{1} is simple
;

for b_{1} being _Graph st b_{1} is loopless & b_{1} is non-Dmulti holds

b_{1} is Dsimple
;

for b_{1} being _Graph st b_{1} is Dsimple holds

( b_{1} is loopless & b_{1} is non-Dmulti )
;

for b_{1} being _Graph st b_{1} is trivial & b_{1} is loopless holds

b_{1} is finite

for b_{1} being _Graph st b_{1} is trivial & b_{1} is non-Dmulti holds

b_{1} is finite
end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] non-multi -> non-Dmulti for _Graph;

coherence for b

b

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] simple -> loopless non-multi for _Graph;

coherence for b

( b

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-multi -> simple for _Graph;

coherence for b

b

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-Dmulti -> Dsimple for _Graph;

coherence for b

b

cluster Relation-like NAT -defined Function-like finite [Graph-like] Dsimple -> loopless non-Dmulti for _Graph;

coherence for b

( b

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless trivial -> finite for _Graph;

coherence for b

b

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial non-Dmulti -> finite for _Graph;

coherence for b

b

proof end;

registration

existence

ex b_{1} being _Graph st

( b_{1} is trivial & b_{1} is simple )

ex b_{1} being _Graph st

( b_{1} is finite & not b_{1} is trivial & b_{1} is simple )

end;
ex b

( b

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial simple for _Graph;

existence ex b

( b

proof end;

registration

let G be finite _Graph;

coherence

the_Vertices_of G is finite by Def17;

coherence

the_Edges_of G is finite by Def17;

end;
coherence

the_Vertices_of G is finite by Def17;

coherence

the_Edges_of G is finite by Def17;

registration

let V be non empty finite set ;

let E be finite set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is finite by FINSEQ_4:76;

end;
let E be finite set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is finite by FINSEQ_4:76;

registration

let V be non empty set ;

let E be empty set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is simple

end;
let E be empty set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is simple

proof end;

registration

let v, E be set ;

let S, T be Function of E,{v};

coherence

createGraph ({v},E,S,T) is trivial

end;
let S, T be Function of E,{v};

coherence

createGraph ({v},E,S,T) is trivial

proof end;

:: deftheorem defines .order() GLIB_000:def 24 :

for G being _Graph holds G .order() = card (the_Vertices_of G);

for G being _Graph holds G .order() = card (the_Vertices_of G);

definition

let G be finite _Graph;

:: original: .order()

redefine func G .order() -> non zero Element of NAT ;

coherence

G .order() is non zero Element of NAT

end;
:: original: .order()

redefine func G .order() -> non zero Element of NAT ;

coherence

G .order() is non zero Element of NAT

proof end;

:: deftheorem defines .size() GLIB_000:def 25 :

for G being _Graph holds G .size() = card (the_Edges_of G);

for G being _Graph holds G .size() = card (the_Edges_of G);

definition

let G be finite _Graph;

:: original: .size()

redefine func G .size() -> Element of NAT ;

coherence

G .size() is Element of NAT

end;
:: original: .size()

redefine func G .size() -> Element of NAT ;

coherence

G .size() is Element of NAT

proof end;

definition

let G be _Graph;

let X be set ;

ex b_{1} being Subset of (the_Edges_of G) st

for e being set holds

( e in b_{1} iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e being set holds

( e in b_{1} iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) & ( for e being set holds

( e in b_{2} iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of (the_Edges_of G) st

for e being set holds

( e in b_{1} iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e being set holds

( e in b_{1} iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) & ( for e being set holds

( e in b_{2} iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func G .edgesInto X -> Subset of (the_Edges_of G) means :Def26: :: GLIB_000:def 26

for e being set holds

( e in it iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) );

existence for e being set holds

( e in it iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) );

ex b

for e being set holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

func G .edgesOutOf X -> Subset of (the_Edges_of G) means :Def27: :: GLIB_000:def 27

for e being set holds

( e in it iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) );

existence for e being set holds

( e in it iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) );

ex b

for e being set holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

:: deftheorem Def26 defines .edgesInto GLIB_000:def 26 :

for G being _Graph

for X being set

for b_{3} being Subset of (the_Edges_of G) holds

( b_{3} = G .edgesInto X iff for e being set holds

( e in b_{3} iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) );

for G being _Graph

for X being set

for b

( b

( e in b

:: deftheorem Def27 defines .edgesOutOf GLIB_000:def 27 :

for G being _Graph

for X being set

for b_{3} being Subset of (the_Edges_of G) holds

( b_{3} = G .edgesOutOf X iff for e being set holds

( e in b_{3} iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) );

for G being _Graph

for X being set

for b

( b

( e in b

definition

let G be _Graph;

let X be set ;

(G .edgesInto X) \/ (G .edgesOutOf X) is Subset of (the_Edges_of G) ;

(G .edgesInto X) /\ (G .edgesOutOf X) is Subset of (the_Edges_of G) ;

end;
let X be set ;

func G .edgesInOut X -> Subset of (the_Edges_of G) equals :: GLIB_000:def 28

(G .edgesInto X) \/ (G .edgesOutOf X);

coherence (G .edgesInto X) \/ (G .edgesOutOf X);

(G .edgesInto X) \/ (G .edgesOutOf X) is Subset of (the_Edges_of G) ;

func G .edgesBetween X -> Subset of (the_Edges_of G) equals :: GLIB_000:def 29

(G .edgesInto X) /\ (G .edgesOutOf X);

coherence (G .edgesInto X) /\ (G .edgesOutOf X);

(G .edgesInto X) /\ (G .edgesOutOf X) is Subset of (the_Edges_of G) ;

:: deftheorem defines .edgesInOut GLIB_000:def 28 :

for G being _Graph

for X being set holds G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X);

for G being _Graph

for X being set holds G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X);

:: deftheorem defines .edgesBetween GLIB_000:def 29 :

for G being _Graph

for X being set holds G .edgesBetween X = (G .edgesInto X) /\ (G .edgesOutOf X);

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 ;

ex b_{1} being Subset of (the_Edges_of G) st

for e being object holds

( e in b_{1} iff e SJoins X,Y,G )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e being object holds

( e in b_{1} iff e SJoins X,Y,G ) ) & ( for e being object holds

( e in b_{2} iff e SJoins X,Y,G ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of (the_Edges_of G) st

for e being object holds

( e in b_{1} iff e DSJoins X,Y,G )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e being object holds

( e in b_{1} iff e DSJoins X,Y,G ) ) & ( for e being object holds

( e in b_{2} iff e DSJoins X,Y,G ) ) holds

b_{1} = b_{2}

end;
let X, Y be set ;

func G .edgesBetween (X,Y) -> Subset of (the_Edges_of G) means :Def30: :: GLIB_000:def 30

for e being object holds

( e in it iff e SJoins X,Y,G );

existence for e being object holds

( e in it iff e SJoins X,Y,G );

ex b

for e being object holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

func G .edgesDBetween (X,Y) -> Subset of (the_Edges_of G) means :Def31: :: GLIB_000:def 31

for e being object holds

( e in it iff e DSJoins X,Y,G );

existence for e being object holds

( e in it iff e DSJoins X,Y,G );

ex b

for e being object holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

:: deftheorem Def30 defines .edgesBetween GLIB_000:def 30 :

for G being _Graph

for X, Y being set

for b_{4} being Subset of (the_Edges_of G) holds

( b_{4} = G .edgesBetween (X,Y) iff for e being object holds

( e in b_{4} iff e SJoins X,Y,G ) );

for G being _Graph

for X, Y being set

for b

( b

( e in b

:: deftheorem Def31 defines .edgesDBetween GLIB_000:def 31 :

for G being _Graph

for X, Y being set

for b_{4} being Subset of (the_Edges_of G) holds

( b_{4} = G .edgesDBetween (X,Y) iff for e being object holds

( e in b_{4} iff e DSJoins X,Y,G ) );

for G being _Graph

for X, Y being set

for b

( b

( e in b

scheme :: GLIB_000:sch 1

FinGraphOrderInd{ P_{1}[ finite _Graph] } :

provided

FinGraphOrderInd{ P

provided

A1:
for G being finite _Graph st G .order() = 1 holds

P_{1}[G]
and

A2: for k being non zero Nat st ( for Gk being finite _Graph st Gk .order() = k holds

P_{1}[Gk] ) holds

for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds

P_{1}[Gk1]

P

A2: for k being non zero Nat st ( for Gk being finite _Graph st Gk .order() = k holds

P

for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds

P

proof end;

scheme :: GLIB_000:sch 2

FinGraphSizeInd{ P_{1}[ finite _Graph] } :

provided

FinGraphSizeInd{ P

provided

A1:
for G being finite _Graph st G .size() = 0 holds

P_{1}[G]
and

A2: for k being Nat st ( for Gk being finite _Graph st Gk .size() = k holds

P_{1}[Gk] ) holds

for Gk1 being finite _Graph st Gk1 .size() = k + 1 holds

P_{1}[Gk1]

P

A2: for k being Nat st ( for Gk being finite _Graph st Gk .size() = k holds

P

for Gk1 being finite _Graph st Gk1 .size() = k + 1 holds

P

proof end;

definition

let G be _Graph;

ex b_{1} being _Graph st

( the_Vertices_of b_{1} c= the_Vertices_of G & the_Edges_of b_{1} c= the_Edges_of G & ( for e being set st e in the_Edges_of b_{1} holds

( (the_Source_of b_{1}) . e = (the_Source_of G) . e & (the_Target_of b_{1}) . e = (the_Target_of G) . e ) ) )

end;
mode Subgraph of G -> _Graph means :Def32: :: GLIB_000:def 32

( the_Vertices_of it c= the_Vertices_of G & the_Edges_of it c= the_Edges_of G & ( for e being set st e in the_Edges_of it holds

( (the_Source_of it) . e = (the_Source_of G) . e & (the_Target_of it) . e = (the_Target_of G) . e ) ) );

existence ( the_Vertices_of it c= the_Vertices_of G & the_Edges_of it c= the_Edges_of G & ( for e being set st e in the_Edges_of it holds

( (the_Source_of it) . e = (the_Source_of G) . e & (the_Target_of it) . e = (the_Target_of G) . e ) ) );

ex b

( the_Vertices_of b

( (the_Source_of b

proof end;

:: deftheorem Def32 defines Subgraph GLIB_000:def 32 :

for G, b_{2} being _Graph holds

( b_{2} is Subgraph of G iff ( the_Vertices_of b_{2} c= the_Vertices_of G & the_Edges_of b_{2} c= the_Edges_of G & ( for e being set st e in the_Edges_of b_{2} holds

( (the_Source_of b_{2}) . e = (the_Source_of G) . e & (the_Target_of b_{2}) . e = (the_Target_of G) . e ) ) ) );

for G, b

( b

( (the_Source_of b

definition

let G1 be _Graph;

let G2 be Subgraph of G1;

:: original: the_Vertices_of

redefine func the_Vertices_of G2 -> non empty Subset of (the_Vertices_of G1);

coherence

the_Vertices_of G2 is non empty Subset of (the_Vertices_of G1) by Def32;

:: original: the_Edges_of

redefine func the_Edges_of G2 -> Subset of (the_Edges_of G1);

coherence

the_Edges_of G2 is Subset of (the_Edges_of G1) by Def32;

end;
let G2 be Subgraph of G1;

:: original: the_Vertices_of

redefine func the_Vertices_of G2 -> non empty Subset of (the_Vertices_of G1);

coherence

the_Vertices_of G2 is non empty Subset of (the_Vertices_of G1) by Def32;

:: original: the_Edges_of

redefine func the_Edges_of G2 -> Subset of (the_Edges_of G1);

coherence

the_Edges_of G2 is Subset of (the_Edges_of G1) by Def32;

registration

let G be _Graph;

ex b_{1} being Subgraph of G st

( b_{1} is trivial & b_{1} is simple )

end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial simple for Subgraph of G;

existence ex b

( b

proof end;

Lm3: for G being _Graph holds G is Subgraph of G

proof end;

Lm4: for G1 being _Graph

for G2 being Subgraph of G1

for x, y, e being object st e Joins x,y,G2 holds

e Joins x,y,G1

proof end;

registration
end;

registration

let G be loopless _Graph;

coherence

for b_{1} being Subgraph of G holds b_{1} is loopless

end;
coherence

for b

proof end;

registration
end;

registration

let G be non-multi _Graph;

coherence

for b_{1} being Subgraph of G holds b_{1} is non-multi

end;
coherence

for b

proof end;

:: deftheorem Def33 defines spanning GLIB_000:def 33 :

for G1 being _Graph

for G2 being Subgraph of G1 holds

( G2 is spanning iff the_Vertices_of G2 = the_Vertices_of G1 );

for G1 being _Graph

for G2 being Subgraph of G1 holds

( G2 is spanning iff the_Vertices_of G2 = the_Vertices_of G1 );

registration
end;

definition

let G1, G2 be _Graph;

for G1 being _Graph holds

( the_Vertices_of G1 = the_Vertices_of G1 & the_Edges_of G1 = the_Edges_of G1 & the_Source_of G1 = the_Source_of G1 & the_Target_of G1 = the_Target_of G1 ) ;

symmetry

for G1, G2 being _Graph st 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 holds

( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 = the_Source_of G1 & the_Target_of G2 = the_Target_of G1 ) ;

end;
pred G1 == G2 means :: GLIB_000:def 34

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

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

for G1 being _Graph holds

( the_Vertices_of G1 = the_Vertices_of G1 & the_Edges_of G1 = the_Edges_of G1 & the_Source_of G1 = the_Source_of G1 & the_Target_of G1 = the_Target_of G1 ) ;

symmetry

for G1, G2 being _Graph st 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 holds

( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of G1 & the_Source_of G2 = the_Source_of G1 & the_Target_of G2 = the_Target_of G1 ) ;

:: deftheorem defines == GLIB_000:def 34 :

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

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

definition
end;

:: deftheorem defines c= GLIB_000:def 35 :

for G1, G2 being _Graph holds

( G1 c= G2 iff G1 is Subgraph of G2 );

for G1, G2 being _Graph holds

( G1 c= G2 iff G1 is Subgraph of G2 );

definition
end;

:: deftheorem defines c< GLIB_000:def 36 :

for G1, G2 being _Graph holds

( G1 c< G2 iff ( G1 c= G2 & G1 != G2 ) );

for G1, G2 being _Graph holds

( G1 c< G2 iff ( G1 c= G2 & G1 != G2 ) );

definition

let G be _Graph;

let V, E be set ;

( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ex b_{1} being Subgraph of G st

( the_Vertices_of b_{1} = V & the_Edges_of b_{1} = E ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b_{1} being Subgraph of G st b_{1} == G ) )

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

end;
let V, E be set ;

mode inducedSubgraph of G,V,E -> Subgraph of G means :Def37: :: GLIB_000:def 37

( the_Vertices_of it = V & the_Edges_of it = E ) if ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V )

otherwise it == G;

existence ( the_Vertices_of it = V & the_Edges_of it = E ) if ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V )

otherwise it == G;

( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ex b

( the_Vertices_of b

proof end;

consistency for b

:: deftheorem Def37 defines inducedSubgraph GLIB_000:def 37 :

for G being _Graph

for V, E being set

for b_{4} being Subgraph of G holds

( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ( b_{4} is inducedSubgraph of G,V,E iff ( the_Vertices_of b_{4} = V & the_Edges_of b_{4} = E ) ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ( b_{4} is inducedSubgraph of G,V,E iff b_{4} == G ) ) );

for G being _Graph

for V, E being set

for b

( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ( b

definition

let G be _Graph;

let V be set ;

mode inducedSubgraph of G,V is inducedSubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedSubgraph of G,V is inducedSubgraph of G,V,G .edgesBetween V;

registration

let G be _Graph;

let V be non empty finite Subset of (the_Vertices_of G);

let E be finite Subset of (G .edgesBetween V);

coherence

for b_{1} being inducedSubgraph of G,V,E holds b_{1} is finite
by Def37;

end;
let V be non empty finite Subset of (the_Vertices_of G);

let E be finite Subset of (G .edgesBetween V);

coherence

for b

registration

let G be _Graph;

let v be Element of the_Vertices_of G;

let E be Subset of (G .edgesBetween {v});

coherence

for b_{1} being inducedSubgraph of G,{v},E holds b_{1} is trivial

end;
let v be Element of the_Vertices_of G;

let E be Subset of (G .edgesBetween {v});

coherence

for b

proof end;

registration

let G be _Graph;

let v be Element of the_Vertices_of G;

coherence

for b_{1} being inducedSubgraph of G,{v}, {} holds

( b_{1} is finite & b_{1} is trivial )

end;
let v be Element of the_Vertices_of G;

coherence

for b

( b

proof end;

registration

let G be _Graph;

let V be non empty Subset of (the_Vertices_of G);

coherence

for b_{1} being inducedSubgraph of G,V, {} holds b_{1} is simple

end;
let V be non empty Subset of (the_Vertices_of G);

coherence

for b

proof end;

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

proof end;

Lm6: for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G)

proof end;

registration

let G be _Graph;

let E be Subset of (the_Edges_of G);

coherence

for b_{1} being inducedSubgraph of G, the_Vertices_of G,E holds b_{1} is spanning

end;
let E be Subset of (the_Edges_of G);

coherence

for b

proof end;

registration

let G be _Graph;

coherence

for b_{1} being inducedSubgraph of G, the_Vertices_of G, {} holds b_{1} is spanning

end;
coherence

for b

proof end;

definition

let G be _Graph;

let v be set ;

mode removeVertex of G,v is inducedSubgraph of G,((the_Vertices_of G) \ {v});

end;
let v be set ;

mode removeVertex of G,v is inducedSubgraph of G,((the_Vertices_of G) \ {v});

definition

let G be _Graph;

let V be set ;

mode removeVertices of G,V is inducedSubgraph of G,((the_Vertices_of G) \ V);

end;
let V be set ;

mode removeVertices of G,V is inducedSubgraph of G,((the_Vertices_of G) \ V);

definition

let G be _Graph;

let e be set ;

mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};

end;
let e be set ;

mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};

definition

let G be _Graph;

let E be set ;

mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;

end;
let E be set ;

mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;

registration

let G be _Graph;

let e be set ;

coherence

for b_{1} being removeEdge of G,e holds b_{1} is spanning
;

end;
let e be set ;

coherence

for b

registration

let G be _Graph;

let E be set ;

coherence

for b_{1} being removeEdges of G,E holds b_{1} is spanning
;

end;
let E be set ;

coherence

for b

definition

let G be _Graph;

let v be Vertex of G;

coherence

G .edgesInto {v} is Subset of (the_Edges_of G) ;

coherence

G .edgesOutOf {v} is Subset of (the_Edges_of G) ;

coherence

G .edgesInOut {v} is Subset of (the_Edges_of G) ;

end;
let v be Vertex of G;

coherence

G .edgesInto {v} is Subset of (the_Edges_of G) ;

coherence

G .edgesOutOf {v} is Subset of (the_Edges_of G) ;

coherence

G .edgesInOut {v} is Subset of (the_Edges_of G) ;

:: deftheorem defines .edgesIn() GLIB_000:def 38 :

for G being _Graph

for v being Vertex of G holds v .edgesIn() = G .edgesInto {v};

for G being _Graph

for v being Vertex of G holds v .edgesIn() = G .edgesInto {v};

:: deftheorem defines .edgesOut() GLIB_000:def 39 :

for G being _Graph

for v being Vertex of G holds v .edgesOut() = G .edgesOutOf {v};

for G being _Graph

for v being Vertex of G holds v .edgesOut() = G .edgesOutOf {v};

:: deftheorem defines .edgesInOut() GLIB_000:def 40 :

for G being _Graph

for v being Vertex of G holds v .edgesInOut() = G .edgesInOut {v};

for G being _Graph

for v being Vertex of G holds v .edgesInOut() = G .edgesInOut {v};

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

proof end;

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

proof end;

definition

let G be _Graph;

let v be Vertex of G;

let e be object ;

( ( e in the_Edges_of G & (the_Target_of G) . e = v implies (the_Source_of G) . e is Vertex of G ) & ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v implies (the_Target_of G) . e is Vertex of G ) & ( ( 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 is Vertex of G ) ) by FUNCT_2:5;

consistency

for b_{1} being Vertex of G st e in the_Edges_of G & (the_Target_of G) . e = v & e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v holds

( b_{1} = (the_Source_of G) . e iff b_{1} = (the_Target_of G) . e )
;

end;
let v be Vertex of G;

let e be object ;

func v .adj e -> Vertex of G equals :Def41: :: GLIB_000:def 41

(the_Source_of G) . e if ( e in the_Edges_of G & (the_Target_of G) . e = v )

(the_Target_of G) . e if ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v )

otherwise v;

coherence (the_Source_of G) . e if ( e in the_Edges_of G & (the_Target_of G) . e = v )

(the_Target_of G) . e if ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v )

otherwise v;

( ( e in the_Edges_of G & (the_Target_of G) . e = v implies (the_Source_of G) . e is Vertex of G ) & ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v implies (the_Target_of G) . e is Vertex of G ) & ( ( 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 is Vertex of G ) ) by FUNCT_2:5;

consistency

for b

( b

:: deftheorem Def41 defines .adj GLIB_000:def 41 :

for G being _Graph

for v being Vertex of G

for e being object 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 ) );

for G being _Graph

for v being Vertex of G

for e being object 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 ) );

definition

let G be _Graph;

let v be Vertex of G;

coherence

card (v .edgesIn()) is Cardinal ;

coherence

card (v .edgesOut()) is Cardinal ;

end;
let v be Vertex of G;

coherence

card (v .edgesIn()) is Cardinal ;

coherence

card (v .edgesOut()) is Cardinal ;

:: deftheorem defines .inDegree() GLIB_000:def 42 :

for G being _Graph

for v being Vertex of G holds v .inDegree() = card (v .edgesIn());

for G being _Graph

for v being Vertex of G holds v .inDegree() = card (v .edgesIn());

:: deftheorem defines .outDegree() GLIB_000:def 43 :

for G being _Graph

for v being Vertex of G holds v .outDegree() = card (v .edgesOut());

for G being _Graph

for v being Vertex of G holds v .outDegree() = card (v .edgesOut());

definition

let G be finite _Graph;

let v be Vertex of G;

:: original: .inDegree()

redefine func v .inDegree() -> Element of NAT ;

coherence

v .inDegree() is Element of NAT

redefine func v .outDegree() -> Element of NAT ;

coherence

v .outDegree() is Element of NAT

end;
let v be Vertex of G;

:: original: .inDegree()

redefine func v .inDegree() -> Element of NAT ;

coherence

v .inDegree() is Element of NAT

proof end;

:: original: .outDegree()redefine func v .outDegree() -> Element of NAT ;

coherence

v .outDegree() is Element of NAT

proof end;

definition
end;

:: deftheorem defines .degree() GLIB_000:def 44 :

for G being _Graph

for v being Vertex of G holds v .degree() = (v .inDegree()) +` (v .outDegree());

for G being _Graph

for v being Vertex of G holds v .degree() = (v .inDegree()) +` (v .outDegree());

definition

let G be finite _Graph;

let v be Vertex of G;

coherence

v .degree() is Element of NAT ;

compatibility

for b_{1} being Element of NAT holds

( b_{1} = v .degree() iff b_{1} = (v .inDegree()) + (v .outDegree()) );

end;
let v be Vertex of G;

:: original: .degree()

redefine func v .degree() -> Element of NAT equals :: GLIB_000:def 45

(v .inDegree()) + (v .outDegree());

correctness redefine func v .degree() -> Element of NAT equals :: GLIB_000:def 45

(v .inDegree()) + (v .outDegree());

coherence

v .degree() is Element of NAT ;

compatibility

for b

( b

proof end;

:: deftheorem defines .degree() GLIB_000:def 45 :

for G being finite _Graph

for v being Vertex of G holds v .degree() = (v .inDegree()) + (v .outDegree());

for G being finite _Graph

for v being Vertex of G holds v .degree() = (v .inDegree()) + (v .outDegree());

definition

let G be _Graph;

let v be Vertex of G;

(the_Source_of G) .: (v .edgesIn()) is Subset of (the_Vertices_of G) ;

(the_Target_of G) .: (v .edgesOut()) is Subset of (the_Vertices_of G) ;

end;
let v be Vertex of G;

func v .inNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 46

(the_Source_of G) .: (v .edgesIn());

coherence (the_Source_of G) .: (v .edgesIn());

(the_Source_of G) .: (v .edgesIn()) is Subset of (the_Vertices_of G) ;

func v .outNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 47

(the_Target_of G) .: (v .edgesOut());

coherence (the_Target_of G) .: (v .edgesOut());

(the_Target_of G) .: (v .edgesOut()) is Subset of (the_Vertices_of G) ;

:: deftheorem defines .inNeighbors() GLIB_000:def 46 :

for G being _Graph

for v being Vertex of G holds v .inNeighbors() = (the_Source_of G) .: (v .edgesIn());

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

for G being _Graph

for v being Vertex of G holds v .outNeighbors() = (the_Target_of G) .: (v .edgesOut());

for G being _Graph

for v being Vertex of G holds v .outNeighbors() = (the_Target_of G) .: (v .edgesOut());

definition

let G be _Graph;

let v be Vertex of G;

(v .inNeighbors()) \/ (v .outNeighbors()) is Subset of (the_Vertices_of G) ;

end;
let v be Vertex of G;

func v .allNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 48

(v .inNeighbors()) \/ (v .outNeighbors());

coherence (v .inNeighbors()) \/ (v .outNeighbors());

(v .inNeighbors()) \/ (v .outNeighbors()) is Subset of (the_Vertices_of G) ;

:: deftheorem defines .allNeighbors() GLIB_000:def 48 :

for G being _Graph

for v being Vertex of G holds v .allNeighbors() = (v .inNeighbors()) \/ (v .outNeighbors());

for G being _Graph

for v being Vertex of G holds v .allNeighbors() = (v .inNeighbors()) \/ (v .outNeighbors());

:: deftheorem defines isolated GLIB_000:def 49 :

for G being _Graph

for v being Vertex of G holds

( v is isolated iff v .edgesInOut() = {} );

for G being _Graph

for v being Vertex of G holds

( v is isolated iff v .edgesInOut() = {} );

definition

let G be finite _Graph;

let v be Vertex of G;

compatibility

( v is isolated iff v .degree() = 0 )

end;
let v be Vertex of G;

compatibility

( v is isolated iff v .degree() = 0 )

proof end;

:: deftheorem defines isolated GLIB_000:def 50 :

for G being finite _Graph

for v being Vertex of G holds

( v is isolated iff v .degree() = 0 );

for G being finite _Graph

for v being Vertex of G holds

( v is isolated iff v .degree() = 0 );

definition

let G be _Graph;

let v be Vertex of G;

end;
let v be Vertex of G;

attr v is endvertex means :: GLIB_000:def 51

ex e being object st

( v .edgesInOut() = {e} & not e Joins v,v,G );

ex e being object st

( v .edgesInOut() = {e} & not e Joins v,v,G );

:: deftheorem defines endvertex GLIB_000:def 51 :

for G being _Graph

for v being Vertex of G holds

( v is endvertex iff ex e being object st

( v .edgesInOut() = {e} & not e Joins v,v,G ) );

for G being _Graph

for v being Vertex of G holds

( v is endvertex iff ex e being object st

( v .edgesInOut() = {e} & not e Joins v,v,G ) );

definition

let G be finite _Graph;

let v be Vertex of G;

compatibility

( v is endvertex iff v .degree() = 1 )

end;
let v be Vertex of G;

compatibility

( v is endvertex iff v .degree() = 1 )

proof end;

:: deftheorem defines endvertex GLIB_000:def 52 :

for G being finite _Graph

for v being Vertex of G holds

( v is endvertex iff v .degree() = 1 );

for G being finite _Graph

for v being Vertex of G holds

( v is endvertex iff v .degree() = 1 );

LmNat: for F being ManySortedSet of NAT

for n being object holds

( n is Nat iff n in dom F )

proof end;

definition

let F be Function;

end;
attr F is Graph-yielding means :Def53a: :: GLIB_000:def 53

for x being object st x in dom F holds

F . x is _Graph;

for x being object st x in dom F holds

F . x is _Graph;

:: deftheorem Def53a defines Graph-yielding GLIB_000:def 53 :

for F being Function holds

( F is Graph-yielding iff for x being object st x in dom F holds

F . x is _Graph );

for F being Function holds

( F is Graph-yielding iff for x being object st x in dom F holds

F . x is _Graph );

definition

let F be ManySortedSet of NAT ;

( F is Graph-yielding iff for n being Nat holds F . n is _Graph )

end;
redefine attr F is Graph-yielding means :Def53: :: GLIB_000:def 54

for n being Nat holds F . n is _Graph;

compatibility for n being Nat holds F . n is _Graph;

( F is Graph-yielding iff for n being Nat holds F . n is _Graph )

proof end;

:: deftheorem Def53 defines Graph-yielding GLIB_000:def 54 :

for F being ManySortedSet of NAT holds

( F is Graph-yielding iff for n being Nat holds F . n is _Graph );

for F being ManySortedSet of NAT holds

( F is Graph-yielding iff for n being Nat holds F . n is _Graph );

:: deftheorem defines halting GLIB_000:def 55 :

for F being ManySortedSet of NAT holds

( F is halting iff ex n being Nat st F . n = F . (n + 1) );

for F being ManySortedSet of NAT holds

( F is halting iff ex n being Nat st F . n = F . (n + 1) );

definition

let F be ManySortedSet of NAT ;

( ( F is halting implies ex b_{1} being Element of NAT st

( F . b_{1} = F . (b_{1} + 1) & ( for n being Nat st F . n = F . (n + 1) holds

b_{1} <= n ) ) ) & ( not F is halting implies ex b_{1} being Element of NAT st b_{1} = 0 ) )

for b_{1}, b_{2} being Element of NAT holds

( ( F is halting & F . b_{1} = F . (b_{1} + 1) & ( for n being Nat st F . n = F . (n + 1) holds

b_{1} <= n ) & F . b_{2} = F . (b_{2} + 1) & ( for n being Nat st F . n = F . (n + 1) holds

b_{2} <= n ) implies b_{1} = b_{2} ) & ( not F is halting & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Element of NAT holds verum
;

end;
func F .Lifespan() -> Element of NAT means :: GLIB_000:def 56

( F . it = F . (it + 1) & ( for n being Nat st F . n = F . (n + 1) holds

it <= n ) ) if F is halting

otherwise it = 0 ;

existence ( F . it = F . (it + 1) & ( for n being Nat st F . n = F . (n + 1) holds

it <= n ) ) if F is halting

otherwise it = 0 ;

( ( F is halting implies ex b

( F . b

b

proof end;

uniqueness for b

( ( F is halting & F . b

b

b

proof end;

consistency for b

:: deftheorem defines .Lifespan() GLIB_000:def 56 :

for F being ManySortedSet of NAT

for b_{2} being Element of NAT holds

( ( F is halting implies ( b_{2} = F .Lifespan() iff ( F . b_{2} = F . (b_{2} + 1) & ( for n being Nat st F . n = F . (n + 1) holds

b_{2} <= n ) ) ) ) & ( not F is halting implies ( b_{2} = F .Lifespan() iff b_{2} = 0 ) ) );

for F being ManySortedSet of NAT

for b

( ( F is halting implies ( b

b

:: deftheorem defines .Result() GLIB_000:def 57 :

for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan());

for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan());

registration
end;

registration

for b_{1} being GraphSeq holds not b_{1} is empty
end;

cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding -> non empty for GraphSeq;

coherence for b

proof end;

registration
end;

registration

let GF be non empty Graph-yielding Function;

let x be Element of dom GF;

coherence

( GF . x is Function-like & GF . x is Relation-like ) by Def53a;

end;
let x be Element of dom GF;

coherence

( GF . x is Function-like & GF . x is Relation-like ) by Def53a;

registration

let GSq be GraphSeq;

let x be Nat;

coherence

( GSq . x is Function-like & GSq . x is Relation-like ) by Def53;

end;
let x be Nat;

coherence

( GSq . x is Function-like & GSq . x is Relation-like ) by Def53;

registration

let GF be non empty Graph-yielding Function;

let x be Element of dom GF;

coherence

( GF . x is NAT -defined & GF . x is finite ) by Def53a;

end;
let x be Element of dom GF;

coherence

( GF . x is NAT -defined & GF . x is finite ) by Def53a;

registration

let GSq be GraphSeq;

let x be Nat;

coherence

( GSq . x is NAT -defined & GSq . x is finite ) by Def53;

end;
let x be Nat;

coherence

( GSq . x is NAT -defined & GSq . x is finite ) by Def53;

registration

let GF be non empty Graph-yielding Function;

let x be Element of dom GF;

coherence

GF . x is [Graph-like] by Def53a;

end;
let x be Element of dom GF;

coherence

GF . x is [Graph-like] by Def53a;

definition

let GF be Graph-yielding Function;

end;
attr GF is finite means :: GLIB_000:def 58

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is finite );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is finite );

attr GF is loopless means :: GLIB_000:def 59

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is loopless );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is loopless );

attr GF is trivial means :: GLIB_000:def 60

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is trivial );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is trivial );

attr GF is non-trivial means :: GLIB_000:def 61

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & not G is trivial );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & not G is trivial );

attr GF is non-multi means :: GLIB_000:def 62

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-multi );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-multi );

attr GF is non-Dmulti means :: GLIB_000:def 63

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-Dmulti );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-Dmulti );

:: deftheorem defines finite GLIB_000:def 58 :

for GF being Graph-yielding Function holds

( GF is finite iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is finite ) );

for GF being Graph-yielding Function holds

( GF is finite iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is finite ) );

:: deftheorem defines loopless GLIB_000:def 59 :

for GF being Graph-yielding Function holds

( GF is loopless iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is loopless ) );

for GF being Graph-yielding Function holds

( GF is loopless iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is loopless ) );

:: deftheorem defines trivial GLIB_000:def 60 :

for GF being Graph-yielding Function holds

( GF is trivial iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is trivial ) );

for GF being Graph-yielding Function holds

( GF is trivial iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is trivial ) );

:: deftheorem defines non-trivial GLIB_000:def 61 :

for GF being Graph-yielding Function holds

( GF is non-trivial iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & not G is trivial ) );

for GF being Graph-yielding Function holds

( GF is non-trivial iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & not G is trivial ) );

:: deftheorem defines non-multi GLIB_000:def 62 :

for GF being Graph-yielding Function holds

( GF is non-multi iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-multi ) );

for GF being Graph-yielding Function holds

( GF is non-multi iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-multi ) );

:: deftheorem defines non-Dmulti GLIB_000:def 63 :

for GF being Graph-yielding Function holds

( GF is non-Dmulti iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-Dmulti ) );

for GF being Graph-yielding Function holds

( GF is non-Dmulti iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is non-Dmulti ) );

:: deftheorem defines simple GLIB_000:def 64 :

for GF being Graph-yielding Function holds

( GF is simple iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is simple ) );

for GF being Graph-yielding Function holds

( GF is simple iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is simple ) );

:: deftheorem defines Dsimple GLIB_000:def 65 :

for GF being Graph-yielding Function holds

( GF is Dsimple iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is Dsimple ) );

for GF being Graph-yielding Function holds

( GF is Dsimple iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is Dsimple ) );

registration

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

( b_{1} is finite & b_{1} is loopless & b_{1} is trivial & b_{1} is non-trivial & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple )
end;

cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding finite loopless trivial non-trivial non-multi non-Dmulti simple Dsimple for Function;

coherence for b

( b

proof end;

definition

let GF be non empty Graph-yielding Function;

( GF is finite iff for x being Element of dom GF holds GF . x is finite )

( GF is loopless iff for x being Element of dom GF holds GF . x is loopless )

( GF is trivial iff for x being Element of dom GF holds GF . x is trivial )

( GF is non-trivial iff for x being Element of dom GF holds not GF . x is trivial )

( GF is non-multi iff for x being Element of dom GF holds GF . x is non-multi )

( GF is non-Dmulti iff for x being Element of dom GF holds GF . x is non-Dmulti )

( GF is simple iff for x being Element of dom GF holds GF . x is simple )

( GF is Dsimple iff for x being Element of dom GF holds GF . x is Dsimple )

end;
redefine attr GF is finite means :Def57b: :: GLIB_000:def 66

for x being Element of dom GF holds GF . x is finite ;

compatibility for x being Element of dom GF holds GF . x is finite ;

( GF is finite iff for x being Element of dom GF holds GF . x is finite )

proof end;

redefine attr GF is loopless means :Def58b: :: GLIB_000:def 67

for x being Element of dom GF holds GF . x is loopless ;

compatibility for x being Element of dom GF holds GF . x is loopless ;

( GF is loopless iff for x being Element of dom GF holds GF . x is loopless )

proof end;

redefine attr GF is trivial means :Def59b: :: GLIB_000:def 68

for x being Element of dom GF holds GF . x is trivial ;

compatibility for x being Element of dom GF holds GF . x is trivial ;

( GF is trivial iff for x being Element of dom GF holds GF . x is trivial )

proof end;

redefine attr GF is non-trivial means :Def60b: :: GLIB_000:def 69

for x being Element of dom GF holds not GF . x is trivial ;

compatibility for x being Element of dom GF holds not GF . x is trivial ;

( GF is non-trivial iff for x being Element of dom GF holds not GF . x is trivial )

proof end;

redefine attr GF is non-multi means :Def61b: :: GLIB_000:def 70

for x being Element of dom GF holds GF . x is non-multi ;

compatibility for x being Element of dom GF holds GF . x is non-multi ;

( GF is non-multi iff for x being Element of dom GF holds GF . x is non-multi )

proof end;

redefine attr GF is non-Dmulti means :Def62b: :: GLIB_000:def 71

for x being Element of dom GF holds GF . x is non-Dmulti ;

compatibility for x being Element of dom GF holds GF . x is non-Dmulti ;

( GF is non-Dmulti iff for x being Element of dom GF holds GF . x is non-Dmulti )

proof end;

redefine attr GF is simple means :Def63b: :: GLIB_000:def 72

for x being Element of dom GF holds GF . x is simple ;

compatibility for x being Element of dom GF holds GF . x is simple ;

( GF is simple iff for x being Element of dom GF holds GF . x is simple )

proof end;

redefine attr GF is Dsimple means :Def64b: :: GLIB_000:def 73

for x being Element of dom GF holds GF . x is Dsimple ;

compatibility for x being Element of dom GF holds GF . x is Dsimple ;

( GF is Dsimple iff for x being Element of dom GF holds GF . x is Dsimple )

proof end;

:: deftheorem Def57b defines finite GLIB_000:def 66 :

for GF being non empty Graph-yielding Function holds

( GF is finite iff for x being Element of dom GF holds GF . x is finite );

for GF being non empty Graph-yielding Function holds

( GF is finite iff for x being Element of dom GF holds GF . x is finite );

:: deftheorem Def58b defines loopless GLIB_000:def 67 :

for GF being non empty Graph-yielding Function holds

( GF is loopless iff for x being Element of dom GF holds GF . x is loopless );

for GF being non empty Graph-yielding Function holds

( GF is loopless iff for x being Element of dom GF holds GF . x is loopless );

:: deftheorem Def59b defines trivial GLIB_000:def 68 :

for GF being non empty Graph-yielding Function holds

( GF is trivial iff for x being Element of dom GF holds GF . x is trivial );

for GF being non empty Graph-yielding Function holds

( GF is trivial iff for x being Element of dom GF holds GF . x is trivial );

:: deftheorem Def60b defines non-trivial GLIB_000:def 69 :

for GF being non empty Graph-yielding Function holds

( GF is non-trivial iff for x being Element of dom GF holds not GF . x is trivial );

for GF being non empty Graph-yielding Function holds

( GF is non-trivial iff for x being Element of dom GF holds not GF . x is trivial );

:: deftheorem Def61b defines non-multi GLIB_000:def 70 :

for GF being non empty Graph-yielding Function holds

( GF is non-multi iff for x being Element of dom GF holds GF . x is non-multi );

for GF being non empty Graph-yielding Function holds

( GF is non-multi iff for x being Element of dom GF holds GF . x is non-multi );

:: deftheorem Def62b defines non-Dmulti GLIB_000:def 71 :

for GF being non empty Graph-yielding Function holds

( GF is non-Dmulti iff for x being Element of dom GF holds GF . x is non-Dmulti );

for GF being non empty Graph-yielding Function holds

( GF is non-Dmulti iff for x being Element of dom GF holds GF . x is non-Dmulti );

:: deftheorem Def63b defines simple GLIB_000:def 72 :

for GF being non empty Graph-yielding Function holds

( GF is simple iff for x being Element of dom GF holds GF . x is simple );

for GF being non empty Graph-yielding Function holds

( GF is simple iff for x being Element of dom GF holds GF . x is simple );

:: deftheorem Def64b defines Dsimple GLIB_000:def 73 :

for GF being non empty Graph-yielding Function holds

( GF is Dsimple iff for x being Element of dom GF holds GF . x is Dsimple );

for GF being non empty Graph-yielding Function holds

( GF is Dsimple iff for x being Element of dom GF holds GF . x is Dsimple );

definition

let GSq be GraphSeq;

( GSq is finite iff for x being Nat holds GSq . x is finite )

( GSq is loopless iff for x being Nat holds GSq . x is loopless )

( GSq is trivial iff for x being Nat holds GSq . x is trivial )

( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial )

( GSq is non-multi iff for x being Nat holds GSq . x is non-multi )

( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti )

( GSq is simple iff for x being Nat holds GSq . x is simple )

( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple )

end;
redefine attr GSq is finite means :Def57: :: GLIB_000:def 74

for x being Nat holds GSq . x is finite ;

compatibility for x being Nat holds GSq . x is finite ;

( GSq is finite iff for x being Nat holds GSq . x is finite )

proof end;

redefine attr GSq is loopless means :Def58: :: GLIB_000:def 75

for x being Nat holds GSq . x is loopless ;

compatibility for x being Nat holds GSq . x is loopless ;

( GSq is loopless iff for x being Nat holds GSq . x is loopless )

proof end;

redefine attr GSq is trivial means :Def59: :: GLIB_000:def 76

for x being Nat holds GSq . x is trivial ;

compatibility for x being Nat holds GSq . x is trivial ;

( GSq is trivial iff for x being Nat holds GSq . x is trivial )

proof end;

redefine attr GSq is non-trivial means :Def60: :: GLIB_000:def 77

for x being Nat holds not GSq . x is trivial ;

compatibility for x being Nat holds not GSq . x is trivial ;

( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial )

proof end;

redefine attr GSq is non-multi means :Def61: :: GLIB_000:def 78

for x being Nat holds GSq . x is non-multi ;

compatibility for x being Nat holds GSq . x is non-multi ;

( GSq is non-multi iff for x being Nat holds GSq . x is non-multi )

proof end;

redefine attr GSq is non-Dmulti means :Def62: :: GLIB_000:def 79

for x being Nat holds GSq . x is non-Dmulti ;

compatibility for x being Nat holds GSq . x is non-Dmulti ;

( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti )

proof end;

redefine attr GSq is simple means :Def63: :: GLIB_000:def 80

for x being Nat holds GSq . x is simple ;

compatibility for x being Nat holds GSq . x is simple ;

( GSq is simple iff for x being Nat holds GSq . x is simple )

proof end;

redefine attr GSq is Dsimple means :Def64: :: GLIB_000:def 81

for x being Nat holds GSq . x is Dsimple ;

compatibility for x being Nat holds GSq . x is Dsimple ;

( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple )

proof end;

:: deftheorem Def57 defines finite GLIB_000:def 74 :

for GSq being GraphSeq holds

( GSq is finite iff for x being Nat holds GSq . x is finite );

for GSq being GraphSeq holds

( GSq is finite iff for x being Nat holds GSq . x is finite );

:: deftheorem Def58 defines loopless GLIB_000:def 75 :

for GSq being GraphSeq holds

( GSq is loopless iff for x being Nat holds GSq . x is loopless );

for GSq being GraphSeq holds

( GSq is loopless iff for x being Nat holds GSq . x is loopless );

:: deftheorem Def59 defines trivial GLIB_000:def 76 :

for GSq being GraphSeq holds

( GSq is trivial iff for x being Nat holds GSq . x is trivial );

for GSq being GraphSeq holds

( GSq is trivial iff for x being Nat holds GSq . x is trivial );

:: deftheorem Def60 defines non-trivial GLIB_000:def 77 :

for GSq being GraphSeq holds

( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial );

for GSq being GraphSeq holds

( GSq is non-trivial iff for x being Nat holds not GSq . x is trivial );

:: deftheorem Def61 defines non-multi GLIB_000:def 78 :

for GSq being GraphSeq holds

( GSq is non-multi iff for x being Nat holds GSq . x is non-multi );

for GSq being GraphSeq holds

( GSq is non-multi iff for x being Nat holds GSq . x is non-multi );

:: deftheorem Def62 defines non-Dmulti GLIB_000:def 79 :

for GSq being GraphSeq holds

( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti );

for GSq being GraphSeq holds

( GSq is non-Dmulti iff for x being Nat holds GSq . x is non-Dmulti );

:: deftheorem Def63 defines simple GLIB_000:def 80 :

for GSq being GraphSeq holds

( GSq is simple iff for x being Nat holds GSq . x is simple );

for GSq being GraphSeq holds

( GSq is simple iff for x being Nat holds GSq . x is simple );

:: deftheorem Def64 defines Dsimple GLIB_000:def 81 :

for GSq being GraphSeq holds

( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple );

for GSq being GraphSeq holds

( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple );

definition

let GSq be GraphSeq;

compatibility

( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) ) ;

end;
compatibility

( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) ) ;

:: deftheorem defines halting GLIB_000:def 82 :

for GSq being GraphSeq holds

( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) );

for GSq being GraphSeq holds

( GSq is halting iff ex n being Nat st GSq . n = GSq . (n + 1) );

registration

ex b_{1} being GraphSeq st

( b_{1} is halting & b_{1} is finite & b_{1} is loopless & b_{1} is trivial & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple )

ex b_{1} being GraphSeq st

( b_{1} is halting & b_{1} is finite & b_{1} is loopless & b_{1} is non-trivial & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple )
end;

cluster non empty Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting finite loopless trivial non-multi non-Dmulti simple Dsimple for GraphSeq;

existence ex b

( b

proof end;

cluster non empty Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting finite loopless non-trivial non-multi non-Dmulti simple Dsimple for GraphSeq;

existence ex b

( b

proof end;

registration

let GF be non empty Graph-yielding finite Function;

let x be Element of dom GF;

coherence

GF . x is finite by Def57b;

end;
let x be Element of dom GF;

coherence

GF . x is finite by Def57b;

registration

let GF be non empty Graph-yielding loopless Function;

let x be Element of dom GF;

coherence

GF . x is loopless by Def58b;

end;
let x be Element of dom GF;

coherence

GF . x is loopless by Def58b;

registration

let GSq be loopless GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is loopless
by Def58;

end;
let x be Nat;

coherence

for b

b

registration

let GF be non empty Graph-yielding trivial Function;

let x be Element of dom GF;

coherence

GF . x is trivial by Def59b;

end;
let x be Element of dom GF;

coherence

GF . x is trivial by Def59b;

registration

let GSq be trivial GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is trivial
by Def59;

end;
let x be Nat;

coherence

for b

b

registration

let GF be non empty Graph-yielding non-trivial Function;

let x be Element of dom GF;

coherence

not GF . x is trivial by Def60b;

end;
let x be Element of dom GF;

coherence

not GF . x is trivial by Def60b;

registration

let GSq be non-trivial GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

not b_{1} is trivial
by Def60;

end;
let x be Nat;

coherence

for b

not b

registration

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

let x be Element of dom GF;

coherence

GF . x is non-multi by Def61b;

end;
let x be Element of dom GF;

coherence

GF . x is non-multi by Def61b;

registration

let GSq be non-multi GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is non-multi
by Def61;

end;
let x be Nat;

coherence

for b

b

registration

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

let x be Element of dom GF;

coherence

GF . x is non-Dmulti by Def62b;

end;
let x be Element of dom GF;

coherence

GF . x is non-Dmulti by Def62b;

registration

let GSq be non-Dmulti GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is non-Dmulti
by Def62;

end;
let x be Nat;

coherence

for b

b

registration

let GF be non empty Graph-yielding simple Function;

let x be Element of dom GF;

coherence

GF . x is simple by Def63b;

end;
let x be Element of dom GF;

coherence

GF . x is simple by Def63b;

registration

let GSq be simple GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is simple
by Def63;

end;
let x be Nat;

coherence

for b

b

registration

let GF be non empty Graph-yielding Dsimple Function;

let x be Element of dom GF;

coherence

GF . x is Dsimple by Def64b;

end;
let x be Element of dom GF;

coherence

GF . x is Dsimple by Def64b;

registration

let GSq be Dsimple GraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is Dsimple
by Def64;

end;
let x be Nat;

coherence

for b

b

registration

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

b_{1} is non-Dmulti
end;

cluster Relation-like Function-like Graph-yielding non-multi -> Graph-yielding non-Dmulti for Function;

coherence for b

b

proof end;

registration

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

( b_{1} is loopless & b_{1} is non-multi )
end;

cluster Relation-like Function-like Graph-yielding simple -> Graph-yielding loopless non-multi for Function;

coherence for b

( b

proof end;

registration

for b_{1} being Graph-yielding Function st b_{1} is loopless & b_{1} is non-multi holds

b_{1} is simple
end;

cluster Relation-like Function-like Graph-yielding loopless non-multi -> Graph-yielding simple for Function;

coherence for b

b

proof end;

registration

for b_{1} being Graph-yielding Function st b_{1} is loopless & b_{1} is non-Dmulti holds

b_{1} is Dsimple
end;

cluster Relation-like Function-like Graph-yielding loopless non-Dmulti -> Graph-yielding Dsimple for Function;

coherence for b

b

proof end;

registration

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

( b_{1} is loopless & b_{1} is non-Dmulti )
end;

cluster Relation-like Function-like Graph-yielding Dsimple -> Graph-yielding loopless non-Dmulti for Function;

coherence for b

( b

proof end;

registration

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

b_{1} is finite
end;

cluster Relation-like Function-like Graph-yielding loopless trivial -> Graph-yielding finite for Function;

coherence for b

b

proof end;

registration

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

b_{1} is finite
end;

cluster Relation-like Function-like Graph-yielding trivial non-Dmulti -> Graph-yielding finite for Function;

coherence for b

b

proof end;

theorem :: GLIB_000:1

theorem :: GLIB_000:3

for GS being GraphStruct holds

( the_Vertices_of GS = GS . VertexSelector & the_Edges_of GS = GS . EdgeSelector & the_Source_of GS = GS . SourceSelector & the_Target_of GS = GS . TargetSelector ) ;

( the_Vertices_of GS = GS . VertexSelector & the_Edges_of GS = GS . EdgeSelector & the_Source_of GS = GS . SourceSelector & the_Target_of GS = GS . TargetSelector ) ;

theorem :: GLIB_000:4

for G being _Graph holds

( dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) = the_Edges_of G & rng (the_Source_of G) c= the_Vertices_of G & rng (the_Target_of G) c= the_Vertices_of G ) by FUNCT_2:def 1;

( dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) = the_Edges_of G & rng (the_Source_of G) c= the_Vertices_of G & rng (the_Target_of G) c= the_Vertices_of G ) by FUNCT_2:def 1;

theorem :: GLIB_000:5

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

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

theorem :: GLIB_000:6

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

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

theorem Th7: :: GLIB_000:7

for GS being GraphStruct

for x being set

for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n}

for x being set

for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n}

proof end;

theorem Th9: :: GLIB_000:9

for GS being GraphStruct

for x being set

for n1, n2 being Nat st n1 <> n2 holds

GS . n2 = (GS .set (n1,x)) . n2

for x being set

for n1, n2 being Nat st n1 <> n2 holds

GS . n2 = (GS .set (n1,x)) . n2

proof end;

theorem :: GLIB_000:10

for G being _Graph

for x being set

for n being Nat st not n in _GraphSelectors holds

( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph )

for x being set

for n being Nat st not n in _GraphSelectors holds

( the_Vertices_of G = the_Vertices_of (G .set (n,x)) & the_Edges_of G = the_Edges_of (G .set (n,x)) & the_Source_of G = the_Source_of (G .set (n,x)) & the_Target_of G = the_Target_of (G .set (n,x)) & G .set (n,x) is _Graph )

proof end;

theorem :: GLIB_000:11

for GS being GraphStruct

for x being set holds

( the_Vertices_of (GS .set (VertexSelector,x)) = x & the_Edges_of (GS .set (EdgeSelector,x)) = x & the_Source_of (GS .set (SourceSelector,x)) = x & the_Target_of (GS .set (TargetSelector,x)) = x ) by Th8;

for x being set holds

( the_Vertices_of (GS .set (VertexSelector,x)) = x & the_Edges_of (GS .set (EdgeSelector,x)) = x & the_Source_of (GS .set (SourceSelector,x)) = x & the_Target_of (GS .set (TargetSelector,x)) = x ) by Th8;

theorem :: GLIB_000:12

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 )

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 )

proof end;

theorem :: GLIB_000:13

for G being _Graph

for e, x, y being object st e Joins x,y,G holds

( x in the_Vertices_of G & y in the_Vertices_of G ) by FUNCT_2:5;

for e, x, y being object st e Joins x,y,G holds

( x in the_Vertices_of G & y in the_Vertices_of G ) by FUNCT_2:5;

theorem :: GLIB_000:14

theorem :: GLIB_000:15

theorem :: GLIB_000:16

theorem :: GLIB_000:17

theorem :: GLIB_000:19

for G being finite loopless _Graph

for v being Vertex of G holds v .degree() = card (v .edgesInOut())

for v being Vertex of G holds v .degree() = card (v .edgesInOut())

proof end;

theorem :: GLIB_000:27

for G being finite _Graph holds

( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} )

( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} )

proof end;

theorem Th28: :: GLIB_000:28

for G being _Graph

for e, X being set holds

( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X )

for e, X being set holds

( ( e in the_Edges_of G & ( (the_Source_of G) . e in X or (the_Target_of G) . e in X ) ) iff e in G .edgesInOut X )

proof end;

theorem :: GLIB_000:29

for G being _Graph

for X being set holds

( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X ) by XBOOLE_0:def 3;

for X being set holds

( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X ) by XBOOLE_0:def 3;

theorem :: GLIB_000:31

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

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

theorem :: GLIB_000:32

theorem Th35: :: GLIB_000:35

for G being _Graph

for X being set holds (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X)

for X being set holds (the_Edges_of G) \ (G .edgesInOut X) = G .edgesBetween ((the_Vertices_of G) \ X)

proof end;

theorem :: GLIB_000:37

for G being _Graph

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds

G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2)

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds

G .edgesBetween (X1,Y1) c= G .edgesBetween (X2,Y2)

proof end;

theorem :: GLIB_000:38

for G being _Graph

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds

G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2)

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds

G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2)

proof end;

theorem :: GLIB_000:39

for G being _Graph

for v being Vertex of G holds

( v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) & v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) )

for v being Vertex of G holds

( v .edgesIn() = G .edgesDBetween ((the_Vertices_of G),{v}) & v .edgesOut() = G .edgesDBetween ({v},(the_Vertices_of G)) )

proof end;

theorem Th41: :: GLIB_000:41

for G1, G2 being _Graph holds

( G1 is Subgraph of G2 & G2 is Subgraph of G1 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 ) )

( G1 is Subgraph of G2 & G2 is Subgraph of G1 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 ) )

proof end;

theorem :: GLIB_000:42

for G1 being _Graph

for G2 being Subgraph of G1

for x being set holds

( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) ) ;

for G2 being Subgraph of G1

for x being set holds

( ( x in the_Vertices_of G2 implies x in the_Vertices_of G1 ) & ( x in the_Edges_of G2 implies x in the_Edges_of G1 ) ) ;

theorem Th43: :: GLIB_000:43

for G1 being _Graph

for G2 being Subgraph of G1

for G3 being Subgraph of G2 holds G3 is Subgraph of G1

for G2 being Subgraph of G1

for G3 being Subgraph of G2 holds G3 is Subgraph of G1

proof end;

theorem Th44: :: GLIB_000:44

for G being _Graph

for G1, G2 being Subgraph of G st the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 holds

G1 is Subgraph of G2

for G1, G2 being Subgraph of G st the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2 holds

G1 is Subgraph of G2

proof end;

theorem Th45: :: GLIB_000:45

for G1 being _Graph

for G2 being Subgraph of G1 holds

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

for G2 being Subgraph of G1 holds

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

proof end;

theorem :: GLIB_000:46

for G being _Graph

for V1, V2, E1, E2 being set

for G1 being inducedSubgraph of G,V1,E1

for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds

G2 is Subgraph of G1

for V1, V2, E1, E2 being set

for G1 being inducedSubgraph of G,V1,E1

for G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non empty Subset of (the_Vertices_of G) & E2 c= G .edgesBetween V2 holds

G2 is Subgraph of G1

proof end;

theorem Th47: :: GLIB_000:47

for G1 being non trivial _Graph

for v being Vertex of G1

for G2 being removeVertex of G1,v holds

( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )

for v being Vertex of G1

for G2 being removeVertex of G1,v holds

( the_Vertices_of G2 = (the_Vertices_of G1) \ {v} & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) )

proof end;

theorem :: GLIB_000:48

for G1 being finite non trivial _Graph

for v being Vertex of G1

for G2 being removeVertex of G1,v holds

( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() )

for v being Vertex of G1

for G2 being removeVertex of G1,v holds

( (G2 .order()) + 1 = G1 .order() & (G2 .size()) + (card (v .edgesInOut())) = G1 .size() )

proof end;

theorem Th49: :: GLIB_000:49

for G1 being _Graph

for V being set

for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds

( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) )

for V being set

for G2 being removeVertices of G1,V st V c< the_Vertices_of G1 holds

( the_Vertices_of G2 = (the_Vertices_of G1) \ V & the_Edges_of G2 = G1 .edgesBetween ((the_Vertices_of G1) \ V) )

proof end;

theorem :: GLIB_000:50

for G1 being finite _Graph

for V being Subset of (the_Vertices_of G1)

for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds

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

for V being Subset of (the_Vertices_of G1)

for G2 being removeVertices of G1,V st V <> the_Vertices_of G1 holds

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

proof end;

theorem Th51: :: GLIB_000:51

for G1 being _Graph

for e being set

for G2 being removeEdge of G1,e holds

( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} )

for e being set

for G2 being removeEdge of G1,e holds

( the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = (the_Edges_of G1) \ {e} )

proof end;

theorem :: GLIB_000:52

for G1 being finite _Graph

for e being set

for G2 being removeEdge of G1,e holds

( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) )

for e being set

for G2 being removeEdge of G1,e holds

( G1 .order() = G2 .order() & ( e in the_Edges_of G1 implies (G2 .size()) + 1 = G1 .size() ) )

proof end;

theorem Th53: :: GLIB_000:53

for G1 being _Graph

for E being set

for G2 being removeEdges of G1,E holds

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

for E being set

for G2 being removeEdges of G1,E holds

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

proof end;

theorem :: GLIB_000:54

theorem :: GLIB_000:55

for G1 being finite _Graph

for E being Subset of (the_Edges_of G1)

for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size()

for E being Subset of (the_Edges_of G1)

for G2 being removeEdges of G1,E holds (G2 .size()) + (card E) = G1 .size()

proof end;

theorem :: GLIB_000:56

for G being _Graph

for e being set

for v being Vertex of G holds

( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) by Lm7;

for e being set

for v being Vertex of G holds

( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) ) by Lm7;

theorem :: GLIB_000:57

for G being _Graph

for e being set

for v being Vertex of G holds

( e in v .edgesIn() iff ex x being set st e DJoins x,v,G )

for e being set

for v being Vertex of G holds

( e in v .edgesIn() iff ex x being set st e DJoins x,v,G )

proof end;

theorem :: GLIB_000:58

for G being _Graph

for e being set

for v being Vertex of G holds

( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) by Lm8;

for e being set

for v being Vertex of G holds

( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) ) by Lm8;

theorem :: GLIB_000:59

for G being _Graph

for e being set

for v being Vertex of G holds

( e in v .edgesOut() iff ex x being set st e DJoins v,x,G )

for e being set

for v being Vertex of G holds

( e in v .edgesOut() iff ex x being set st e DJoins v,x,G )

proof end;

theorem :: GLIB_000:60

for G being _Graph

for v being Vertex of G holds v .edgesInOut() = (v .edgesIn()) \/ (v .edgesOut()) ;

for v being Vertex of G holds v .edgesInOut() = (v .edgesIn()) \/ (v .edgesOut()) ;

theorem Th61: :: GLIB_000:61

for G being _Graph

for e being set

for v being Vertex of G holds

( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) )

for e being set

for v being Vertex of G holds

( e in v .edgesInOut() iff ( e in the_Edges_of G & ( (the_Source_of G) . e = v or (the_Target_of G) . e = v ) ) )

proof end;

theorem Th63: :: GLIB_000:63

for G being _Graph

for e being set

for v1, v2 being Vertex of G holds

( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )

for e being set

for v1, v2 being Vertex of G holds

( not e Joins v1,v2,G or ( e in v1 .edgesIn() & e in v2 .edgesOut() ) or ( e in v2 .edgesIn() & e in v1 .edgesOut() ) )

proof end;

theorem :: GLIB_000:64

for G being _Graph

for e being set

for v1 being Vertex of G holds

( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G )

for e being set

for v1 being Vertex of G holds

( e in v1 .edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G )

proof end;

theorem :: GLIB_000:65

for G being _Graph

for v being Vertex of G

for e, x, y being object st e in v .edgesInOut() & e Joins x,y,G & not v = x holds

v = y

for v being Vertex of G

for e, x, y being object st e in v .edgesInOut() & e Joins x,y,G & not v = x holds

v = y

proof end;

theorem :: GLIB_000:66

for G being _Graph

for v1, v2 being Vertex of G

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

( v1 .adj e = v2 & v2 .adj e = v1 )

for v1, v2 being Vertex of G

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

( v1 .adj e = v2 & v2 .adj e = v1 )

proof end;

theorem :: GLIB_000:67

for G being _Graph

for e being set

for v being Vertex of G holds

( e in v .edgesInOut() iff e Joins v,v .adj e,G )

for e being set

for v being Vertex of G holds

( e in v .edgesInOut() iff e Joins v,v .adj e,G )

proof end;

theorem :: GLIB_000:68

for G being finite _Graph

for e being set

for v1, v2 being Vertex of G st e Joins v1,v2,G holds

( 1 <= v1 .degree() & 1 <= v2 .degree() )

for e being set

for v1, v2 being Vertex of G st e Joins v1,v2,G holds

( 1 <= v1 .degree() & 1 <= v2 .degree() )

proof end;

theorem Th69: :: GLIB_000:69

for G being _Graph

for x being set

for v being Vertex of G holds

( x in v .inNeighbors() iff ex e being object st e DJoins x,v,G )

for x being set

for v being Vertex of G holds

( x in v .inNeighbors() iff ex e being object st e DJoins x,v,G )

proof end;

theorem Th70: :: GLIB_000:70

for G being _Graph

for x being set

for v being Vertex of G holds

( x in v .outNeighbors() iff ex e being object st e DJoins v,x,G )

for x being set

for v being Vertex of G holds

( x in v .outNeighbors() iff ex e being object st e DJoins v,x,G )

proof end;

theorem Th71: :: GLIB_000:71

for G being _Graph

for x being set

for v being Vertex of G holds

( x in v .allNeighbors() iff ex e being object st e Joins v,x,G )

for x being set

for v being Vertex of G holds

( x in v .allNeighbors() iff ex e being object st e Joins v,x,G )

proof end;

theorem Th72: :: GLIB_000:72

for G1 being _Graph

for G2 being Subgraph of G1

for x, y being set

for e being object 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 ) )

for G2 being Subgraph of G1

for x, y being set

for e being object 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 ) )

proof end;

theorem :: GLIB_000:73

theorem :: GLIB_000:74

for G1 being _Graph

for G2 being spanning Subgraph of G1

for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1

for G2 being spanning Subgraph of G1

for G3 being spanning Subgraph of G2 holds G3 is spanning Subgraph of G1

proof end;

theorem :: GLIB_000:75

for G1 being finite _Graph

for G2 being Subgraph of G1 holds

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

for G2 being Subgraph of G1 holds

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

proof end;

theorem :: GLIB_000:76

for G1 being _Graph

for G2 being Subgraph of G1

for X being set holds

( G2 .edgesInto X c= G1 .edgesInto X & G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X )

for G2 being Subgraph of G1

for X being set holds

( G2 .edgesInto X c= G1 .edgesInto X & G2 .edgesOutOf X c= G1 .edgesOutOf X & G2 .edgesInOut X c= G1 .edgesInOut X & G2 .edgesBetween X c= G1 .edgesBetween X )

proof end;

theorem :: GLIB_000:77

for G1 being _Graph

for G2 being Subgraph of G1

for X, Y being set holds

( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) & G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) )

for G2 being Subgraph of G1

for X, Y being set holds

( G2 .edgesBetween (X,Y) c= G1 .edgesBetween (X,Y) & G2 .edgesDBetween (X,Y) c= G1 .edgesDBetween (X,Y) )

proof end;

theorem Th78: :: GLIB_000:78

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() )

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .edgesIn() c= v1 .edgesIn() & v2 .edgesOut() c= v1 .edgesOut() & v2 .edgesInOut() c= v1 .edgesInOut() )

proof end;

theorem Th79: :: GLIB_000:79

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) )

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .edgesIn() = (v1 .edgesIn()) /\ (the_Edges_of G2) & v2 .edgesOut() = (v1 .edgesOut()) /\ (the_Edges_of G2) & v2 .edgesInOut() = (v1 .edgesInOut()) /\ (the_Edges_of G2) )

proof end;

theorem :: GLIB_000:80

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2

for e being set st v1 = v2 & e in the_Edges_of G2 holds

v1 .adj e = v2 .adj e

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2

for e being set st v1 = v2 & e in the_Edges_of G2 holds

v1 .adj e = v2 .adj e

proof end;

theorem :: GLIB_000:81

for G1 being finite _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .inDegree() <= v1 .inDegree() & v2 .outDegree() <= v1 .outDegree() & v2 .degree() <= v1 .degree() )

proof end;

theorem :: GLIB_000:82

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() )

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

( v2 .inNeighbors() c= v1 .inNeighbors() & v2 .outNeighbors() c= v1 .outNeighbors() & v2 .allNeighbors() c= v1 .allNeighbors() )

proof end;

theorem :: GLIB_000:83

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds

v2 is isolated

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds

v2 is isolated

proof end;

theorem :: GLIB_000:84

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds

v2 is isolated

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex & not v2 is endvertex holds

v2 is isolated

proof end;

theorem Th86: :: GLIB_000:86

for G being _Graph

for G1, G2 being Subgraph of G st the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds

G1 == G2

for G1, G2 being Subgraph of G st the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds

G1 == G2

proof end;

theorem :: GLIB_000:88

theorem :: GLIB_000:89

for G1, G2 being _Graph st G1 == G2 holds

( ( G1 is finite implies G2 is finite ) & ( G1 is loopless implies G2 is loopless ) & ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) )

( ( G1 is finite implies G2 is finite ) & ( G1 is loopless implies G2 is loopless ) & ( G1 is trivial implies G2 is trivial ) & ( G1 is non-multi implies G2 is non-multi ) & ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G1 is simple implies G2 is simple ) & ( G1 is Dsimple implies G2 is Dsimple ) )

proof end;

theorem Th90: :: GLIB_000:90

for G1, G2 being _Graph

for X, Y being set st G1 == G2 holds

( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )

for X, Y being set st G1 == G2 holds

( G1 .order() = G2 .order() & G1 .size() = G2 .size() & G1 .edgesInto X = G2 .edgesInto X & G1 .edgesOutOf X = G2 .edgesOutOf X & G1 .edgesInOut X = G2 .edgesInOut X & G1 .edgesBetween X = G2 .edgesBetween X & G1 .edgesDBetween (X,Y) = G2 .edgesDBetween (X,Y) )

proof end;

theorem :: GLIB_000:95

for G1, G2 being _Graph

for V, E being set

for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds

G3 is inducedSubgraph of G2,V,E

for V, E being set

for G3 being inducedSubgraph of G1,V,E st G1 == G2 holds

G3 is inducedSubgraph of G2,V,E

proof end;

theorem Th96: :: GLIB_000:96

for G1, G2 being _Graph

for e being set

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds

( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() )

for e being set

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds

( v1 .edgesIn() = v2 .edgesIn() & v1 .edgesOut() = v2 .edgesOut() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .adj e = v2 .adj e & v1 .inDegree() = v2 .inDegree() & v1 .outDegree() = v2 .outDegree() & v1 .degree() = v2 .degree() & v1 .inNeighbors() = v2 .inNeighbors() & v1 .outNeighbors() = v2 .outNeighbors() & v1 .allNeighbors() = v2 .allNeighbors() )

proof end;

theorem :: GLIB_000:97

for G1, G2 being _Graph

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds

( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) )

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 & G1 == G2 holds

( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) )

proof end;

theorem Th98: :: GLIB_000:98

for G being _Graph

for G1, G2 being Subgraph of G holds

( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )

for G1, G2 being Subgraph of G holds

( not G1 c< G2 or the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2 )

proof end;

theorem :: GLIB_000:99

for G being _Graph

for G1, G2 being Subgraph of G holds

( not G1 c< G2 or ex v being object st

( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st

( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )

for G1, G2 being Subgraph of G holds

( not G1 c< G2 or ex v being object st

( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being object st

( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )

proof end;