:: Alternative Graph Structures
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users

registration

cluster Relation-like NAT -defined Function-like finite for set ;

existence
ex b₁ being Function st
( b₁ is finite & b₁ is NAT -defined )

proof end;

end;

definition

mode GraphStruct is NAT -defined finite Function;

end;

definition

func VertexSelector -> Element of NAT equals :: GLIB_000:def 1
1;

coherence
1 is Element of NAT ;

func EdgeSelector -> Element of NAT equals :: GLIB_000:def 2
2;

coherence
2 is Element of NAT ;

func SourceSelector -> Element of NAT equals :: GLIB_000:def 3
3;

coherence
3 is Element of NAT ;

func TargetSelector -> Element of NAT equals :: GLIB_000:def 4
4;

coherence
4 is Element of NAT ;

end;

:: deftheorem defines VertexSelector GLIB_000:def 1 :
VertexSelector = 1;

:: deftheorem defines EdgeSelector GLIB_000:def 2 :
EdgeSelector = 2;

:: deftheorem defines SourceSelector GLIB_000:def 3 :
SourceSelector = 3;

:: deftheorem defines TargetSelector GLIB_000:def 4 :
TargetSelector = 4;

definition

func _GraphSelectors -> non empty Subset of NAT equals :: GLIB_000:def 5
{VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

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

end;

:: deftheorem defines _GraphSelectors GLIB_000:def 5 :
_GraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector};

definition

let G be GraphStruct;

func the_Vertices_of G -> set equals :: GLIB_000:def 6
G . VertexSelector;

coherence
G . VertexSelector is set ;

func the_Edges_of G -> set equals :: GLIB_000:def 7
G . EdgeSelector;

coherence
G . EdgeSelector is set ;

func the_Source_of G -> set equals :: GLIB_000:def 8
G . SourceSelector;

coherence
G . SourceSelector is set ;

func the_Target_of G -> set equals :: GLIB_000:def 9
G . TargetSelector;

coherence
G . TargetSelector is set ;

end;

:: deftheorem defines the_Vertices_of GLIB_000:def 6 :
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;

:: deftheorem defines the_Source_of GLIB_000:def 8 :
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;

definition

let G be GraphStruct;

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

end;

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

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] for set ;

existence
ex b₁ being GraphStruct st b₁ is [Graph-like]

proof end;

end;

definition

mode _Graph is [Graph-like] GraphStruct;

end;

registration

let G be _Graph;

cluster the_Vertices_of G -> non empty ;

coherence
not the_Vertices_of G is empty by Def10;

end;

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;

definition

let V be non empty set ;
let E be set ;
let S, T be Function of E,V;

func createGraph (V,E,S,T) -> _Graph equals :: GLIB_000:def 11
<*V,E,S,T*>;

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

proof end;

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

definition

let G be GraphStruct;
let n be Nat;
let x be set ;

func G .set (n,x) -> GraphStruct equals :: GLIB_000:def 12
G +* (n .--> x);

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

proof end;

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

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;

registration

let G be _Graph;

cluster G | _GraphSelectors -> [Graph-like] ;

coherence
G | _GraphSelectors is [Graph-like]

proof end;

end;

definition

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

end;

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

definition

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

end;

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

definition

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

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

end;

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

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

definition

let G be _Graph;

attr G is _finite means :Def17: :: GLIB_000:def 17
( 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 );

attr G is _trivial means :Def19: :: GLIB_000:def 19
card (the_Vertices_of G) = 1;

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;

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;

end;

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

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

:: deftheorem Def19 defines _trivial GLIB_000:def 19 :
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 );

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

definition

let G be _Graph;

attr G is simple means :: GLIB_000:def 22
( G is loopless & G is non-multi );

attr G is Dsimple means :: GLIB_000:def 23
( G is loopless & G is non-Dmulti );

end;

:: deftheorem defines simple GLIB_000:def 22 :
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 ) );

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

proof end;

registration

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

coherence
for b₁ being _Graph st b₁ is non-multi holds
b₁ is non-Dmulti

proof end;

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

coherence
for b₁ being _Graph st b₁ is simple holds
( b₁ is loopless & b₁ is non-multi ) ;

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

coherence
for b₁ being _Graph st b₁ is loopless & b₁ is non-multi holds
b₁ is simple ;

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

coherence
for b₁ being _Graph st b₁ is loopless & b₁ is non-Dmulti holds
b₁ is Dsimple ;

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

coherence
for b₁ being _Graph st b₁ is Dsimple holds
( b₁ is loopless & b₁ is non-Dmulti ) ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless _trivial -> _finite for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is loopless holds
b₁ is _finite

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial non-Dmulti -> _finite for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is non-Dmulti holds
b₁ is _finite

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial simple for set ;

existence
ex b₁ being _Graph st
( b₁ is _trivial & b₁ is simple )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite non _trivial simple for set ;

existence
ex b₁ being _Graph st
( b₁ is _finite & not b₁ is _trivial & b₁ is simple )

proof end;

end;

registration

let G be _finite _Graph;

cluster the_Vertices_of G -> finite ;

coherence
the_Vertices_of G is finite by Def17;

cluster the_Edges_of G -> finite ;

coherence
the_Edges_of G is finite by Def17;

end;

registration

let G be _trivial _Graph;

cluster the_Vertices_of G -> finite ;

coherence
the_Vertices_of G is finite

proof end;

end;

registration

let V be non empty finite set ;
let E be finite set ;
let S, T be Function of E,V;

cluster createGraph (V,E,S,T) -> _finite ;

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

end;

registration

let V be non empty set ;
let E be empty set ;
let S, T be Function of E,V;

cluster createGraph (V,E,S,T) -> simple ;

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

proof end;

end;

registration

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

cluster createGraph ({v},E,S,T) -> _trivial ;

coherence
createGraph ({v},E,S,T) is _trivial

proof end;

end;

definition

let G be _Graph;

func G .order() -> Cardinal equals :: GLIB_000:def 24
card (the_Vertices_of G);

coherence
card (the_Vertices_of G) is Cardinal ;

end;

:: deftheorem defines .order() GLIB_000:def 24 :
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

proof end;

end;

definition

let G be _Graph;

func G .size() -> Cardinal equals :: GLIB_000:def 25
card (the_Edges_of G);

coherence
card (the_Edges_of G) is Cardinal ;

end;

:: deftheorem defines .size() GLIB_000:def 25 :
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

proof end;

end;

definition

let G be _Graph;
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
ex b₁ being Subset of (the_Edges_of G) st
for e being set holds
( e in b₁ iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (the_Edges_of G) st ( for e being set holds
( e in b₁ iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) & ( for e being set holds
( e in b₂ iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) holds
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
ex b₁ being Subset of (the_Edges_of G) st
for e being set holds
( e in b₁ iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (the_Edges_of G) st ( for e being set holds
( e in b₁ iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) & ( for e being set holds
( e in b₂ iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def26 defines .edgesInto GLIB_000:def 26 :
for G being _Graph
for X being set
for b₃ being Subset of (the_Edges_of G) holds
( b₃ = G .edgesInto X iff for e being set holds
( e in b₃ iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) );

:: deftheorem Def27 defines .edgesOutOf GLIB_000:def 27 :
for G being _Graph
for X being set
for b₃ being Subset of (the_Edges_of G) holds
( b₃ = G .edgesOutOf X iff for e being set holds
( e in b₃ iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) );

definition

let G be _Graph;
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) 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) is Subset of (the_Edges_of G) ;

end;

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

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

definition

let G be _Graph;
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
ex b₁ being Subset of (the_Edges_of G) st
for e being object holds
( e in b₁ iff e SJoins X,Y,G )

proof end;

uniqueness
for b₁, b₂ being Subset of (the_Edges_of G) st ( for e being object holds
( e in b₁ iff e SJoins X,Y,G ) ) & ( for e being object holds
( e in b₂ iff e SJoins X,Y,G ) ) holds
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
ex b₁ being Subset of (the_Edges_of G) st
for e being object holds
( e in b₁ iff e DSJoins X,Y,G )

proof end;

uniqueness
for b₁, b₂ being Subset of (the_Edges_of G) st ( for e being object holds
( e in b₁ iff e DSJoins X,Y,G ) ) & ( for e being object holds
( e in b₂ iff e DSJoins X,Y,G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def30 defines .edgesBetween GLIB_000:def 30 :
for G being _Graph
for X, Y being set
for b₄ being Subset of (the_Edges_of G) holds
( b₄ = G .edgesBetween (X,Y) iff for e being object holds
( e in b₄ iff e SJoins X,Y,G ) );

:: deftheorem Def31 defines .edgesDBetween GLIB_000:def 31 :
for G being _Graph
for X, Y being set
for b₄ being Subset of (the_Edges_of G) holds
( b₄ = G .edgesDBetween (X,Y) iff for e being object holds
( e in b₄ iff e DSJoins X,Y,G ) );

scheme :: GLIB_000:sch 1
FinGraphOrderInd{ P₁[ _Graph] } :

for G being _finite _Graph holds P₁[G]

provided

A1: for G being _finite _Graph st G .order() = 1 holds
P₁[G] and
A2: for k being non zero Nat st ( for Gk being _finite _Graph st Gk .order() = k holds
P₁[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .order() = k + 1 holds
P₁[Gk1]

proof end;

scheme :: GLIB_000:sch 2
FinGraphSizeInd{ P₁[ _Graph] } :

for G being _finite _Graph holds P₁[G]

provided

A1: for G being _finite _Graph st G .size() = 0 holds
P₁[G] and
A2: for k being Nat st ( for Gk being _finite _Graph st Gk .size() = k holds
P₁[Gk] ) holds
for Gk1 being _finite _Graph st Gk1 .size() = k + 1 holds
P₁[Gk1]

proof end;

definition

let G be _Graph;

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
ex b₁ being _Graph st
( the_Vertices_of b₁ c= the_Vertices_of G & the_Edges_of b₁ c= the_Edges_of G & ( for e being set st e in the_Edges_of b₁ holds
( (the_Source_of b₁) . e = (the_Source_of G) . e & (the_Target_of b₁) . e = (the_Target_of G) . e ) ) )

proof end;

end;

:: deftheorem Def32 defines Subgraph GLIB_000:def 32 :
for G, b₂ being _Graph holds
( b₂ is Subgraph of G iff ( the_Vertices_of b₂ c= the_Vertices_of G & the_Edges_of b₂ c= the_Edges_of G & ( for e being set st e in the_Edges_of b₂ holds
( (the_Source_of b₂) . e = (the_Source_of G) . e & (the_Target_of b₂) . e = (the_Target_of G) . e ) ) ) );

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;

registration

let G be _Graph;

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

existence
ex b₁ being Subgraph of G st
( b₁ is _trivial & b₁ is simple )

proof end;

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

let G be _finite _Graph;

cluster -> _finite for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is _finite

proof end;

end;

registration

let G be loopless _Graph;

cluster -> loopless for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is loopless

proof end;

end;

registration

let G be _trivial _Graph;

cluster -> _trivial for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is _trivial

proof end;

end;

registration

let G be non-multi _Graph;

cluster -> non-multi for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is non-multi

proof end;

end;

definition

let G1 be _Graph;
let G2 be Subgraph of G1;

attr G2 is spanning means :Def33: :: GLIB_000:def 33
the_Vertices_of G2 = the_Vertices_of G1;

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

registration

let G be _Graph;

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

existence
ex b₁ being Subgraph of G st b₁ is spanning

proof end;

end;

definition

let G1, G2 be _Graph;

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

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

notation

let G1, G2 be _Graph;
antonym G1 != G2 for G1 == G2;

end;

definition

let G1, G2 be _Graph;

pred G1 c= G2 means :: GLIB_000:def 35
G1 is Subgraph of G2;

reflexivity
for G1 being _Graph holds G1 is Subgraph of G1 by Lm3;

end;

:: deftheorem defines c= GLIB_000:def 35 :
for G1, G2 being _Graph holds
( G1 c= G2 iff G1 is Subgraph of G2 );

definition

let G1, G2 be _Graph;

pred G1 c< G2 means :: GLIB_000:def 36
( G1 c= G2 & G1 != G2 );

irreflexivity
for G1 being _Graph holds
( not G1 c= G1 or not G1 != G1 ) ;

end;

:: deftheorem defines c< GLIB_000:def 36 :
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 ;

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
( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ex b₁ being Subgraph of G st
( the_Vertices_of b₁ = V & the_Edges_of b₁ = E ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b₁ being Subgraph of G st b₁ == G ) )

proof end;

consistency
for b₁ being Subgraph of G holds verum ;

end;

:: deftheorem Def37 defines inducedSubgraph GLIB_000:def 37 :
for G being _Graph
for V, E being set
for b₄ being Subgraph of G holds
( ( V is non empty Subset of (the_Vertices_of G) & E c= G .edgesBetween V implies ( b₄ is inducedSubgraph of G,V,E iff ( the_Vertices_of b₄ = V & the_Edges_of b₄ = E ) ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ( b₄ is inducedSubgraph of G,V,E iff b₄ == G ) ) );

definition

let G be _Graph;
let V be set ;
mode inducedSubgraph of G,V is inducedSubgraph of G,V,G .edgesBetween V;

end;

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

cluster -> _finite for inducedSubgraph of G,V,E;

coherence
for b₁ being inducedSubgraph of G,V,E holds b₁ is _finite by Def37;

end;

registration

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

cluster -> _trivial for inducedSubgraph of G,{v},E;

coherence
for b₁ being inducedSubgraph of G,{v},E holds b₁ is _trivial

proof end;

end;

registration

let G be _Graph;
let v be Element of the_Vertices_of G;

cluster -> _finite _trivial for inducedSubgraph of G,{v}, {} ;

coherence
for b₁ being inducedSubgraph of G,{v}, {} holds
( b₁ is _finite & b₁ is _trivial )

proof end;

end;

registration

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

cluster -> simple for inducedSubgraph of G,V, {} ;

coherence
for b₁ being inducedSubgraph of G,V, {} holds b₁ is simple

proof end;

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

cluster -> spanning for inducedSubgraph of G, the_Vertices_of G,E;

coherence
for b₁ being inducedSubgraph of G, the_Vertices_of G,E holds b₁ is spanning

proof end;

end;

registration

let G be _Graph;

cluster -> spanning for inducedSubgraph of G, the_Vertices_of G, {} ;

coherence
for b₁ being inducedSubgraph of G, the_Vertices_of G, {} holds b₁ is spanning

proof end;

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;

definition

let G be _Graph;
let V be set ;
mode removeVertices of G,V is inducedSubgraph of G,((the_Vertices_of G) \ V);

end;

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;

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;

registration

let G be _Graph;
let e be set ;

cluster -> spanning for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};

coherence
for b₁ being removeEdge of G,e holds b₁ is spanning ;

end;

registration

let G be _Graph;
let E be set ;

cluster -> spanning for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;

coherence
for b₁ being removeEdges of G,E holds b₁ is spanning ;

end;

definition

let G be _Graph;
mode Vertex of G is Element of the_Vertices_of G;

end;

definition

let G be _Graph;
let v be Vertex of G;

func v .edgesIn() -> Subset of (the_Edges_of G) equals :: GLIB_000:def 38
G .edgesInto {v};

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

func v .edgesOut() -> Subset of (the_Edges_of G) equals :: GLIB_000:def 39
G .edgesOutOf {v};

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

func v .edgesInOut() -> Subset of (the_Edges_of G) equals :: GLIB_000:def 40
G .edgesInOut {v};

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

end;

:: deftheorem defines .edgesIn() GLIB_000:def 38 :
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};

:: deftheorem defines .edgesInOut() GLIB_000:def 40 :
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 ;

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
( ( 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₁ 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₁ = (the_Source_of G) . e iff b₁ = (the_Target_of G) . e ) ;

end;

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

definition

let G be _Graph;
let v be Vertex of G;

func v .inDegree() -> Cardinal equals :: GLIB_000:def 42
card (v .edgesIn());

coherence
card (v .edgesIn()) is Cardinal ;

func v .outDegree() -> Cardinal equals :: GLIB_000:def 43
card (v .edgesOut());

coherence
card (v .edgesOut()) is Cardinal ;

end;

:: deftheorem defines .inDegree() GLIB_000:def 42 :
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());

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

proof end;

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

proof end;

end;

definition

let G be _Graph;
let v be Vertex of G;

func v .degree() -> Cardinal equals :: GLIB_000:def 44
(v .inDegree()) +` (v .outDegree());

coherence
(v .inDegree()) +` (v .outDegree()) is Cardinal ;

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

definition

let G be _finite _Graph;
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
coherence
v .degree() is Element of NAT ;
compatibility
for b₁ being Element of NAT holds
( b₁ = v .degree() iff b₁ = (v .inDegree()) + (v .outDegree()) );

proof end;

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

definition

let G be _Graph;
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()) 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()) is Subset of (the_Vertices_of G) ;

end;

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

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

definition

let G be _Graph;
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()) is Subset of (the_Vertices_of G) ;

end;

:: deftheorem defines .allNeighbors() GLIB_000:def 48 :
for G being _Graph
for v being Vertex of G holds v .allNeighbors() = (v .inNeighbors()) \/ (v .outNeighbors());

definition

let G be _Graph;
let v be Vertex of G;

attr v is isolated means :: GLIB_000:def 49
v .edgesInOut() = {} ;

end;

:: deftheorem defines isolated GLIB_000:def 49 :
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;

redefine attr v is isolated means :: GLIB_000:def 50
v .degree() = 0 ;

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

proof end;

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

definition

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

end;

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

definition

let G be _finite _Graph;
let v be Vertex of G;

redefine attr v is endvertex means :: GLIB_000:def 52
v .degree() = 1;

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

proof end;

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

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;

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;

end;

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

definition

let F be ManySortedSet of NAT ;

redefine attr F is Graph-yielding means :Def53: :: GLIB_000:def 54
for n being Nat holds F . n is _Graph;

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

proof end;

attr F is halting means :: GLIB_000:def 55
ex n being Nat st F . n = F . (n + 1);

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

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

definition

let F be ManySortedSet of NAT ;

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 is halting implies ex b₁ being Element of NAT st
( F . b₁ = F . (b₁ + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b₁ <= n ) ) ) & ( not F is halting implies ex b₁ being Element of NAT st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT holds
( ( F is halting & F . b₁ = F . (b₁ + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b₁ <= n ) & F . b₂ = F . (b₂ + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b₂ <= n ) implies b₁ = b₂ ) & ( not F is halting & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Element of NAT holds verum ;

end;

:: deftheorem defines .Lifespan() GLIB_000:def 56 :
for F being ManySortedSet of NAT
for b₂ being Element of NAT holds
( ( F is halting implies ( b₂ = F .Lifespan() iff ( F . b₂ = F . (b₂ + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b₂ <= n ) ) ) ) & ( not F is halting implies ( b₂ = F .Lifespan() iff b₂ = 0 ) ) );

definition

let F be ManySortedSet of NAT ;

func F .Result() -> set equals :: GLIB_000:def 57
F . (F .Lifespan());

coherence
F . (F .Lifespan()) is set ;

end;

:: deftheorem defines .Result() GLIB_000:def 57 :
for F being ManySortedSet of NAT holds F .Result() = F . (F .Lifespan());

registration

cluster empty Relation-like Function-like -> Graph-yielding for set ;

coherence
for b₁ being Function st b₁ is empty holds
b₁ is Graph-yielding ;

end;

registration

let G be _Graph;

cluster NAT --> G -> Graph-yielding ;

coherence
NAT --> G is Graph-yielding

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding for set ;

existence
ex b₁ being ManySortedSet of NAT st b₁ is Graph-yielding

proof end;

end;

definition

mode GraphSeq is Graph-yielding ManySortedSet of NAT ;

end;

registration

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

coherence
for b₁ being GraphSeq holds not b₁ is empty

proof end;

end;

registration

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

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is Graph-yielding )

proof end;

end;

registration

let GF be non empty Graph-yielding Function;
let x be Element of dom GF;

cluster GF . x -> Relation-like Function-like ;

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

end;

registration

let GSq be GraphSeq;
let x be Nat;

cluster GSq . x -> Relation-like Function-like ;

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

end;

registration

let GF be non empty Graph-yielding Function;
let x be Element of dom GF;

cluster GF . x -> NAT -defined finite ;

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

end;

registration

let GSq be GraphSeq;
let x be Nat;

cluster GSq . x -> NAT -defined finite ;

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

end;

registration

let GF be non empty Graph-yielding Function;
let x be Element of dom GF;

cluster GF . x -> [Graph-like] ;

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

end;

registration

let GSq be GraphSeq;
let x be Nat;

cluster GSq . x -> [Graph-like] ;

coherence
GSq . x is [Graph-like] by Def53;

end;

definition

let GF be Graph-yielding Function;

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

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

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

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

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

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

attr GF is simple means :: GLIB_000:def 64
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is simple );

attr GF is Dsimple means :: GLIB_000:def 65
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is Dsimple );

end;

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

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

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

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

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

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

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

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

registration

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

coherence
for b₁ being Graph-yielding Function st b₁ is empty holds
( b₁ is _finite & b₁ is loopless & b₁ is _trivial & b₁ is non-trivial & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple ) ;

end;

definition

let GF be non empty Graph-yielding Function;

redefine attr GF is _finite means :Def57b: :: GLIB_000:def 66
for x being Element of dom GF holds GF . x is _finite ;

compatibility
( 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
( 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
( 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
( 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
( 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
( 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
( 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
( GF is Dsimple iff for x being Element of dom GF holds GF . x is Dsimple )

proof end;

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

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

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

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

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

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

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

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

definition

let GSq be GraphSeq;

redefine attr GSq is _finite means :Def57: :: GLIB_000:def 74
for x being Nat holds GSq . x is _finite ;

compatibility
( 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
( 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
( 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
( 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
( 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
( 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
( 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
( GSq is Dsimple iff for x being Nat holds GSq . x is Dsimple )

proof end;

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

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

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

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

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

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

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

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

definition

let GSq be GraphSeq;

redefine attr GSq is halting means :: GLIB_000:def 82
ex n being Nat st GSq . n = GSq . (n + 1);

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

end;

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

registration

cluster non empty Relation-like NAT -defined Function-like V17( NAT ) Graph-yielding halting _finite loopless _trivial non-multi non-Dmulti simple Dsimple for set ;

existence
ex b₁ being GraphSeq st
( b₁ is halting & b₁ is _finite & b₁ is loopless & b₁ is _trivial & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple )

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

existence
ex b₁ being GraphSeq st
( b₁ is halting & b₁ is _finite & b₁ is loopless & b₁ is non-trivial & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple )

proof end;

end;

registration

let GF be non empty Graph-yielding _finite Function;
let x be Element of dom GF;

cluster GF . x -> _finite ;

coherence
GF . x is _finite by Def57b;

end;

registration

let GSq be _finite GraphSeq;
let x be Nat;

cluster GSq . x -> _finite ;

coherence
GSq . x is _finite by Def57;

end;

registration

let GF be non empty Graph-yielding loopless Function;
let x be Element of dom GF;

cluster GF . x -> loopless ;

coherence
GF . x is loopless by Def58b;

end;

registration

let GSq be loopless GraphSeq;
let x be Nat;

cluster GSq . x -> loopless for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is loopless by Def58;

end;

registration

let GF be non empty Graph-yielding _trivial Function;
let x be Element of dom GF;

cluster GF . x -> _trivial ;

coherence
GF . x is _trivial by Def59b;

end;

registration

let GSq be _trivial GraphSeq;
let x be Nat;

cluster GSq . x -> _trivial for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is _trivial by Def59;

end;

registration

let GF be non empty Graph-yielding non-trivial Function;
let x be Element of dom GF;

cluster GF . x -> non _trivial ;

coherence
not GF . x is _trivial by Def60b;

end;

registration

let GSq be non-trivial GraphSeq;
let x be Nat;

cluster GSq . x -> non _trivial for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
not b₁ is _trivial by Def60;

end;

registration

let GF be non empty Graph-yielding non-multi Function;
let x be Element of dom GF;

cluster GF . x -> non-multi ;

coherence
GF . x is non-multi by Def61b;

end;

registration

let GSq be non-multi GraphSeq;
let x be Nat;

cluster GSq . x -> non-multi for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is non-multi by Def61;

end;

registration

let GF be non empty Graph-yielding non-Dmulti Function;
let x be Element of dom GF;

cluster GF . x -> non-Dmulti ;

coherence
GF . x is non-Dmulti by Def62b;

end;

registration

let GSq be non-Dmulti GraphSeq;
let x be Nat;

cluster GSq . x -> non-Dmulti for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is non-Dmulti by Def62;

end;

registration

let GF be non empty Graph-yielding simple Function;
let x be Element of dom GF;

cluster GF . x -> simple ;

coherence
GF . x is simple by Def63b;

end;

registration

let GSq be simple GraphSeq;
let x be Nat;

cluster GSq . x -> simple for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is simple by Def63;

end;

registration

let GF be non empty Graph-yielding Dsimple Function;
let x be Element of dom GF;

cluster GF . x -> Dsimple ;

coherence
GF . x is Dsimple by Def64b;

end;

registration

let GSq be Dsimple GraphSeq;
let x be Nat;

cluster GSq . x -> Dsimple for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is Dsimple by Def64;

end;

registration

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

coherence
for b₁ being Graph-yielding Function st b₁ is non-multi holds
b₁ is non-Dmulti

proof end;

end;

registration

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

coherence
for b₁ being Graph-yielding Function st b₁ is simple holds
( b₁ is loopless & b₁ is non-multi )

proof end;

end;

registration

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

coherence
for b₁ being Graph-yielding Function st b₁ is loopless & b₁ is non-multi holds
b₁ is simple

proof end;

end;

registration

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

coherence
for b₁ being Graph-yielding Function st b₁ is loopless & b₁ is non-Dmulti holds
b₁ is Dsimple

proof end;

end;

registration

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

coherence
for b₁ being Graph-yielding Function st b₁ is Dsimple holds
( b₁ is loopless & b₁ is non-Dmulti )

proof end;

end;

registration

cluster Relation-like Function-like Graph-yielding loopless _trivial -> Graph-yielding _finite for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is _trivial & b₁ is loopless holds
b₁ is _finite

proof end;

end;

registration

cluster Relation-like Function-like Graph-yielding _trivial non-Dmulti -> Graph-yielding _finite for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is _trivial & b₁ is non-Dmulti holds
b₁ is _finite

proof end;

end;

theorem :: GLIB_000:1

( VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 & TargetSelector = 4 ) ;

theorem :: GLIB_000:2

for G being _Graph holds _GraphSelectors c= dom G

proof end;

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

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;

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;

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;

registration

let V be non empty set ;
let E be set ;
let S, T be Function of E,V;

reduce the_Vertices_of (createGraph (V,E,S,T)) to V;

reducibility
the_Vertices_of (createGraph (V,E,S,T)) = V by FINSEQ_4:76;

reduce the_Edges_of (createGraph (V,E,S,T)) to E;

reducibility
the_Edges_of (createGraph (V,E,S,T)) = E by FINSEQ_4:76;

reduce the_Source_of (createGraph (V,E,S,T)) to S;

reducibility
the_Source_of (createGraph (V,E,S,T)) = S by FINSEQ_4:76;

reduce the_Target_of (createGraph (V,E,S,T)) to T;

reducibility
the_Target_of (createGraph (V,E,S,T)) = T by FINSEQ_4:76;

end;

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}

proof end;

theorem Th8: :: GLIB_000:8

for GS being GraphStruct
for x being set
for n being Nat holds (GS .set (n,x)) . n = x

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

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 )

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;

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 )

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;

theorem :: GLIB_000:14

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

theorem :: GLIB_000:15

for G being _Graph
for e, x1, x2, y1, y2 being object st e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) holds
( x1 = y2 & y1 = x2 ) ;

theorem :: GLIB_000:16

for G being _Graph
for e, x, y being object holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) ;

theorem :: GLIB_000:17

for G being _Graph
for X, Y being set
for e, x, y being object st e Joins x,y,G & ( ( x in X & y in Y ) or ( x in Y & y in X ) ) holds
e SJoins X,Y,G ;

theorem :: GLIB_000:18

for G being _Graph holds
( G is loopless iff for v, e being object holds not e Joins v,v,G )

proof end;

theorem :: GLIB_000:19

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

proof end;

theorem :: GLIB_000:20

for G being non _trivial _Graph
for v being Vertex of G holds not (the_Vertices_of G) \ {v} is empty

proof end;

theorem :: GLIB_000:21

for G being non _trivial _Graph ex v1, v2 being Vertex of G st v1 <> v2

proof end;

theorem Th22: :: GLIB_000:22

for G being _trivial _Graph ex v being Vertex of G st the_Vertices_of G = {v}

proof end;

theorem :: GLIB_000:23

for G being loopless _trivial _Graph holds the_Edges_of G = {}

proof end;

theorem :: GLIB_000:24

for G being _Graph st the_Edges_of G = {} holds
G is simple

proof end;

theorem :: GLIB_000:25

for G being _finite _Graph holds G .order() >= 1

proof end;

theorem :: GLIB_000:26

for G being _Graph holds
( G .order() = 1 iff G is _trivial ) ;

theorem :: GLIB_000:27

for G being _Graph holds
( 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 )

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;

theorem :: GLIB_000:30

for G being _Graph holds the_Edges_of G = G .edgesInOut (the_Vertices_of G)

proof end;

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;

theorem :: GLIB_000:32

for G being _Graph
for X being set
for e, x, y being object st x in X & y in X & e Joins x,y,G holds
e in G .edgesBetween X by Lm5;

theorem :: GLIB_000:33

for G being _Graph
for X being set holds G .edgesBetween X c= G .edgesInOut X

proof end;

theorem Th34: :: GLIB_000:34

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

proof end;

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)

proof end;

theorem :: GLIB_000:36

for G being _Graph
for X, Y being set st X c= Y holds
G .edgesBetween X c= G .edgesBetween Y

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)

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)

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

proof end;

theorem :: GLIB_000:40

for G being _Graph holds G is Subgraph of G by Lm3;

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

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

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

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

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

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

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

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

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

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

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

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

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 )

proof end;

theorem :: GLIB_000:54

for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E holds G1 .order() = G2 .order() by Th53;

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

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;

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 )

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;

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 )

proof end;

theorem :: GLIB_000:60

for G being _Graph
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 ) ) )

proof end;

theorem Th62: :: GLIB_000:62

for G being _Graph
for v1 being Vertex of G
for e, x being object st e Joins v1,x,G holds
e in v1 .edgesInOut() by Th61;

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

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 )

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

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 )

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 )

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

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 )

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 )

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 )

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

proof end;

theorem :: GLIB_000:73

for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e in the_Edges_of G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) ) by Def32;

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

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

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 )

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

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

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

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

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

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

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

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

proof end;

theorem :: GLIB_000:85

for G1, G2, G3 being _Graph st G1 == G2 & G2 == G3 holds
G1 == G3 ;

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

proof end;

theorem Th87: :: GLIB_000:87

for G1, G2 being _Graph holds
( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) ) by Th41;

theorem :: GLIB_000:88

for G1, G2 being _Graph
for X, Y being set
for e, x, y being object st G1 == G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) ) ;

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

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

proof end;

theorem Th91: :: GLIB_000:91

for G1, G2, G3 being _Graph st G1 == G2 & G3 is Subgraph of G1 holds
G3 is Subgraph of G2

proof end;

theorem :: GLIB_000:92

for G1, G2, G3 being _Graph st G1 == G2 & G1 is Subgraph of G3 holds
G2 is Subgraph of G3

proof end;

theorem :: GLIB_000:93

for G being _Graph
for E, V being set
for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2

proof end;

theorem :: GLIB_000:94

for G1 being _Graph
for G2 being inducedSubgraph of G1,(the_Vertices_of G1) holds G1 == G2

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

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

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

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 )

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

proof end;