:: GLIB_000 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
mode GraphStruct -> finite Function means :Def1: :: GLIB_000:def 1
 dom it c= NAT ;
existence
ex b1 being finite Function st dom b1 c= NAT
proof end;
end;

:: deftheorem Def1 defines GraphStruct GLIB_000:def 1 :
for b1 being finite Function holds
( b1 is GraphStruct iff dom b1 c= NAT );

definition
func VertexSelector -> Nat equals :: GLIB_000:def 2
1;
coherence
1 is Nat ;
func EdgeSelector -> Nat equals :: GLIB_000:def 3
2;
coherence
2 is Nat ;
func SourceSelector -> Nat equals :: GLIB_000:def 4
3;
coherence
3 is Nat ;
func TargetSelector -> Nat equals :: GLIB_000:def 5
4;
coherence
4 is Nat ;
end;

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

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

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

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

definition
func _GraphSelectors -> non empty Subset of NAT equals :: GLIB_000:def 6
{VertexSelector ,EdgeSelector ,SourceSelector ,TargetSelector };
coherence
{VertexSelector ,EdgeSelector ,SourceSelector ,TargetSelector } is non empty Subset of NAT by ENUMSET1:def 2;
end;

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

definition
let G be GraphStruct ;
func the_Vertices_of G -> set equals :: GLIB_000:def 7
G . VertexSelector ;
coherence
G . VertexSelector is set ;
func the_Edges_of G -> set equals :: GLIB_000:def 8
G . EdgeSelector ;
coherence
G . EdgeSelector is set ;
func the_Source_of G -> set equals :: GLIB_000:def 9
G . SourceSelector ;
coherence
G . SourceSelector is set ;
func the_Target_of G -> set equals :: GLIB_000:def 10
G . TargetSelector ;
coherence
G . TargetSelector is set ;
end;

:: deftheorem defines the_Vertices_of GLIB_000:def 7 :
for G being GraphStruct holds the_Vertices_of G = G . VertexSelector ;

:: deftheorem defines the_Edges_of GLIB_000:def 8 :
for G being GraphStruct holds the_Edges_of G = G . EdgeSelector ;

:: deftheorem defines the_Source_of GLIB_000:def 9 :
for G being GraphStruct holds the_Source_of G = G . SourceSelector ;

:: deftheorem defines the_Target_of GLIB_000:def 10 :
for G being GraphStruct holds the_Target_of G = G . TargetSelector ;

definition
let G be GraphStruct ;
attr G is [Graph-like] means :Def11: :: GLIB_000:def 11
( 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 Def11 defines [Graph-like] GLIB_000:def 11 :
for G being GraphStruct holds
( G is [Graph-like] iff ( VertexSelector in dom G & EdgeSelector in dom G & SourceSelector in dom G & TargetSelector in dom G & the_Vertices_of G is non empty set & the_Source_of G is Function of the_Edges_of G, the_Vertices_of G & the_Target_of G is Function of the_Edges_of G, the_Vertices_of G ) );

registration
cluster finite [Graph-like] GraphStruct ;
existence
ex b1 being GraphStruct st b1 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 Def11;
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 Def11;
:: 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 Def11;
end;

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

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 12
<*V,E,S,T*>;
coherence
<*V,E,S,T*> is _Graph
proof end;
end;

:: deftheorem defines createGraph GLIB_000:def 12 :
for V being non empty set
for E being set
for S, T being Function of E,V holds createGraph V,E,S,T = <*V,E,S,T*>;

Lm2: 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 SCMPDS_1:3;

registration
let x, y be set ;
cluster x .--> y -> finite ;
coherence
x .--> y is finite
proof end;
end;

definition
let G be GraphStruct ;
let n be Nat;
let x be set ;
func G .set n,x -> GraphStruct equals :: GLIB_000:def 13
G +* (n .--> x);
coherence
G +* (n .--> x) is GraphStruct
proof end;
end;

:: deftheorem defines .set GLIB_000:def 13 :
for G being GraphStruct
for n being Nat
for x being set holds G .set n,x = G +* (n .--> x);

definition
let G be GraphStruct ;
let X be set ;
func G .strict X -> GraphStruct equals :: GLIB_000:def 14
G | X;
coherence
G | X is GraphStruct
proof end;
end;

:: deftheorem defines .strict GLIB_000:def 14 :
for G being GraphStruct
for X being set holds G .strict X = G | X;

Lm3: 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 .strict _GraphSelectors -> finite [Graph-like] ;
coherence
G .strict _GraphSelectors is [Graph-like]
proof end;
end;

definition
let G be _Graph;
let x, y, e be set ;
pred e Joins x,y,G means :Def15: :: GLIB_000:def 15
( 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 Def15 defines Joins GLIB_000:def 15 :
for G being _Graph
for x, y, e being set holds
( e Joins x,y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e = x & (the_Target_of G) . e = y ) or ( (the_Source_of G) . e = y & (the_Target_of G) . e = x ) ) ) );

definition
let G be _Graph;
let x, y, e be set ;
pred e DJoins x,y,G means :Def16: :: GLIB_000:def 16
( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y );
end;

:: deftheorem Def16 defines DJoins GLIB_000:def 16 :
for G being _Graph
for x, y, e being set holds
( e DJoins x,y,G iff ( e in the_Edges_of G & (the_Source_of G) . e = x & (the_Target_of G) . e = y ) );

definition
let G be _Graph;
let X, Y, e be set ;
pred e SJoins X,Y,G means :Def17: :: GLIB_000:def 17
( 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 :Def18: :: GLIB_000:def 18
( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y );
end;

:: deftheorem Def17 defines SJoins GLIB_000:def 17 :
for G being _Graph
for X, Y, e being set holds
( e SJoins X,Y,G iff ( e in the_Edges_of G & ( ( (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) or ( (the_Source_of G) . e in Y & (the_Target_of G) . e in X ) ) ) );

:: deftheorem Def18 defines DSJoins GLIB_000:def 18 :
for G being _Graph
for X, Y, e being set holds
( e DSJoins X,Y,G iff ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in Y ) );

Lm4: for G being _Graph
for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) )
proof end;

definition
let G be _Graph;
attr G is finite means :Def19: :: GLIB_000:def 19
( the_Vertices_of G is finite & the_Edges_of G is finite );
attr G is loopless means :Def20: :: GLIB_000:def 20
for e being set holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e );
attr G is trivial means :Def21: :: GLIB_000:def 21
 Card (the_Vertices_of G) = one ;
attr G is non-multi means :Def22: :: GLIB_000:def 22
for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2;
attr G is non-Dmulti means :Def23: :: GLIB_000:def 23
for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2;
end;

:: deftheorem Def19 defines finite GLIB_000:def 19 :
for G being _Graph holds
( G is finite iff ( the_Vertices_of G is finite & the_Edges_of G is finite ) );

:: deftheorem Def20 defines loopless GLIB_000:def 20 :
for G being _Graph holds
( G is loopless iff for e being set holds
( not e in the_Edges_of G or not (the_Source_of G) . e = (the_Target_of G) . e ) );

:: deftheorem Def21 defines trivial GLIB_000:def 21 :
for G being _Graph holds
( G is trivial iff Card (the_Vertices_of G) = one );

:: deftheorem Def22 defines non-multi GLIB_000:def 22 :
for G being _Graph holds
( G is non-multi iff for e1, e2, v1, v2 being set st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2 );

:: deftheorem Def23 defines non-Dmulti GLIB_000:def 23 :
for G being _Graph holds
( G is non-Dmulti iff for e1, e2, v1, v2 being set st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G holds
e1 = e2 );

definition
let G be _Graph;
attr G is simple means :Def24: :: GLIB_000:def 24
( G is loopless & G is non-multi );
attr G is Dsimple means :Def25: :: GLIB_000:def 25
( G is loopless & G is non-Dmulti );
end;

:: deftheorem Def24 defines simple GLIB_000:def 24 :
for G being _Graph holds
( G is simple iff ( G is loopless & G is non-multi ) );

:: deftheorem Def25 defines Dsimple GLIB_000:def 25 :
for G being _Graph holds
( G is Dsimple iff ( G is loopless & G is non-Dmulti ) );

Lm5: for G being _Graph st the_Edges_of G = {} holds
G is simple
proof end;

registration
cluster non-multi -> non-Dmulti GraphStruct ;
coherence
for b1 being _Graph st b1 is non-multi holds
b1 is non-Dmulti
proof end;
cluster simple -> loopless non-multi GraphStruct ;
coherence
for b1 being _Graph st b1 is simple holds
( b1 is loopless & b1 is non-multi ) by Def24;
cluster loopless non-multi -> simple GraphStruct ;
coherence
for b1 being _Graph st b1 is loopless & b1 is non-multi holds
b1 is simple by Def24;
cluster loopless non-Dmulti -> Dsimple GraphStruct ;
coherence
for b1 being _Graph st b1 is loopless & b1 is non-Dmulti holds
b1 is Dsimple by Def25;
cluster Dsimple -> loopless non-Dmulti GraphStruct ;
coherence
for b1 being _Graph st b1 is Dsimple holds
( b1 is loopless & b1 is non-Dmulti ) by Def25;
cluster loopless trivial -> finite GraphStruct ;
coherence
for b1 being _Graph st b1 is trivial & b1 is loopless holds
b1 is finite
proof end;
cluster trivial non-Dmulti -> finite GraphStruct ;
coherence
for b1 being _Graph st b1 is trivial & b1 is non-Dmulti holds
b1 is finite
proof end;
end;

registration
cluster finite loopless trivial non-multi non-Dmulti simple Dsimple GraphStruct ;
existence
ex b1 being _Graph st
( b1 is trivial & b1 is simple )
proof end;
cluster finite loopless non trivial non-multi non-Dmulti simple Dsimple GraphStruct ;
existence
ex b1 being _Graph st
( b1 is finite & not b1 is trivial & b1 is simple )
proof end;
end;

registration
let G be finite _Graph;
cluster the_Vertices_of G -> non empty finite ;
coherence
the_Vertices_of G is finite by Def19;
cluster the_Edges_of G -> finite ;
coherence
the_Edges_of G is finite by Def19;
end;

registration
let G be trivial _Graph;
cluster the_Vertices_of G -> non empty 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
proof end;
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 -> loopless non-multi non-Dmulti simple Dsimple ;
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 26
 Card (the_Vertices_of G);
coherence
Card (the_Vertices_of G) is Cardinal ;
end;

:: deftheorem defines .order() GLIB_000:def 26 :
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 empty Nat;
coherence
G .order() is non empty Nat
proof end;
end;

definition
let G be _Graph;
func G .size() -> Cardinal equals :: GLIB_000:def 27
 Card (the_Edges_of G);
coherence
Card (the_Edges_of G) is Cardinal ;
end;

:: deftheorem defines .size() GLIB_000:def 27 :
for G being _Graph holds G .size() = Card (the_Edges_of G);

definition
let G be finite _Graph;
:: original: .size()
redefine func G .size() -> Nat;
coherence
G .size() is Nat
proof end;
end;

definition
let G be _Graph;
let X be set ;
func G .edgesInto X -> Subset of (the_Edges_of G) means :Def28: :: GLIB_000:def 28
for e being set holds
( e in it iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) )
proof end;
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) & ( for e being set holds
( e in b2 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) ) holds
b1 = b2
proof end;
func G .edgesOutOf X -> Subset of (the_Edges_of G) means :Def29: :: GLIB_000:def 29
for e being set holds
( e in it iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) )
proof end;
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) & ( for e being set holds
( e in b2 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def28 defines .edgesInto GLIB_000:def 28 :
for G being _Graph
for X being set
for b3 being Subset of (the_Edges_of G) holds
( b3 = G .edgesInto X iff for e being set holds
( e in b3 iff ( e in the_Edges_of G & (the_Target_of G) . e in X ) ) );

:: deftheorem Def29 defines .edgesOutOf GLIB_000:def 29 :
for G being _Graph
for X being set
for b3 being Subset of (the_Edges_of G) holds
( b3 = G .edgesOutOf X iff for e being set holds
( e in b3 iff ( e in the_Edges_of G & (the_Source_of G) . e in X ) ) );

definition
let G be _Graph;
let X be set ;
func G .edgesInOut X -> Subset of (the_Edges_of G) equals :: GLIB_000:def 30
(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 31
(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 30 :
for G being _Graph
for X being set holds G .edgesInOut X = (G .edgesInto X) \/ (G .edgesOutOf X);

:: deftheorem defines .edgesBetween GLIB_000:def 31 :
for G being _Graph
for X being set holds G .edgesBetween X = (G .edgesInto X) /\ (G .edgesOutOf X);

definition
let G be _Graph;
let X, Y be set ;
func G .edgesBetween X,Y -> Subset of (the_Edges_of G) means :Def32: :: GLIB_000:def 32
for e being set holds
( e in it iff e SJoins X,Y,G );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e SJoins X,Y,G )
proof end;
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e SJoins X,Y,G ) ) & ( for e being set holds
( e in b2 iff e SJoins X,Y,G ) ) holds
b1 = b2
proof end;
func G .edgesDBetween X,Y -> Subset of (the_Edges_of G) means :Def33: :: GLIB_000:def 33
for e being set holds
( e in it iff e DSJoins X,Y,G );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e DSJoins X,Y,G )
proof end;
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e DSJoins X,Y,G ) ) & ( for e being set holds
( e in b2 iff e DSJoins X,Y,G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def32 defines .edgesBetween GLIB_000:def 32 :
for G being _Graph
for X, Y being set
for b4 being Subset of (the_Edges_of G) holds
( b4 = G .edgesBetween X,Y iff for e being set holds
( e in b4 iff e SJoins X,Y,G ) );

:: deftheorem Def33 defines .edgesDBetween GLIB_000:def 33 :
for G being _Graph
for X, Y being set
for b4 being Subset of (the_Edges_of G) holds
( b4 = G .edgesDBetween X,Y iff for e being set holds
( e in b4 iff e DSJoins X,Y,G ) );

scheme :: GLIB_000:sch 1
FinGraphOrderInd{ P1[ finite _Graph] } :
for G being finite _Graph holds P1[G]
provided
A1: for G being finite _Graph st G .order() = 1 holds
P1[G] and
A2: for k being non empty Nat st ( for Gk being finite _Graph st Gk .order() = k holds
P1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .order() = k + 1 holds
P1[Gk1]
proof end;

scheme :: GLIB_000:sch 2
FinGraphSizeInd{ P1[ finite _Graph] } :
for G being finite _Graph holds P1[G]
provided
A1: for G being finite _Graph st G .size() = 0 holds
P1[G] and
A2: for k being Nat st ( for Gk being finite _Graph st Gk .size() = k holds
P1[Gk] ) holds
for Gk1 being finite _Graph st Gk1 .size() = k + 1 holds
P1[Gk1]
proof end;

definition
let G be _Graph;
mode Subgraph of G -> _Graph means :Def34: :: GLIB_000:def 34
( 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 b1 being _Graph st
( the_Vertices_of b1 c= the_Vertices_of G & the_Edges_of b1 c= the_Edges_of G & ( for e being set st e in the_Edges_of b1 holds
( (the_Source_of b1) . e = (the_Source_of G) . e & (the_Target_of b1) . e = (the_Target_of G) . e ) ) )
proof end;
end;

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

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 Def34;
:: 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 Def34;
end;

registration
let G be _Graph;
cluster finite loopless trivial non-multi non-Dmulti simple Dsimple Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is trivial & b1 is simple )
proof end;
end;

Lm6: for G being _Graph holds G is Subgraph of G
proof end;

Lm7: for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
e Joins x,y,G1
proof end;

registration
let G be finite _Graph;
cluster -> finite Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is finite
proof end;
end;

registration
let G be loopless _Graph;
cluster -> loopless Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is loopless
proof end;
end;

registration
let G be trivial _Graph;
cluster -> trivial Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is trivial
proof end;
end;

registration
let G be non-multi _Graph;
cluster -> non-multi Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is non-multi
proof end;
end;

definition
let G1 be _Graph;
let G2 be Subgraph of G1;
attr G2 is spanning means :Def35: :: GLIB_000:def 35
 the_Vertices_of G2 = the_Vertices_of G1;
end;

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

registration
let G be _Graph;
cluster spanning Subgraph of G;
existence
ex b1 being Subgraph of G st b1 is spanning
proof end;
end;

definition
let G1, G2 be _Graph;
pred G1 == G2 means :Def36: :: GLIB_000:def 36
( 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 Def36 defines == GLIB_000:def 36 :
for G1, G2 being _Graph holds
( G1 == G2 iff ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2 ) );

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

definition
let G1, G2 be _Graph;
pred G1 c= G2 means :Def37: :: GLIB_000:def 37
G1 is Subgraph of G2;
reflexivity
for G1 being _Graph holds G1 is Subgraph of G1 by Lm6;
end;

:: deftheorem Def37 defines c= GLIB_000:def 37 :
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 :Def38: :: GLIB_000:def 38
( G1 c= G2 & G1 != G2 );
irreflexivity
for G1 being _Graph holds
( not G1 c= G1 or not G1 != G1 ) ;
end;

:: deftheorem Def38 defines c< GLIB_000:def 38 :
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 :Def39: :: GLIB_000:def 39
( 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 b1 being Subgraph of G st
( the_Vertices_of b1 = V & the_Edges_of b1 = E ) ) & ( ( not V is non empty Subset of (the_Vertices_of G) or not E c= G .edgesBetween V ) implies ex b1 being Subgraph of G st b1 == G ) )
proof end;
consistency
for b1 being Subgraph of G holds verum ;
end;

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

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 inducedSubgraph of G,V,E;
coherence
for b1 being inducedSubgraph of G,V,E holds b1 is finite
proof end;
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 inducedSubgraph of G,{v},E;
coherence
for b1 being inducedSubgraph of G,{v},E holds b1 is trivial
proof end;
end;

registration
let G be _Graph;
let v be Element of the_Vertices_of G;
cluster -> finite trivial inducedSubgraph of G,{v}, {} ;
coherence
for b1 being inducedSubgraph of G,{v}, {} holds
( b1 is finite & b1 is trivial )
proof end;
end;

registration
let G be _Graph;
let V be non empty Subset of (the_Vertices_of G);
cluster -> simple inducedSubgraph of G,V, {} ;
coherence
for b1 being inducedSubgraph of G,V, {} holds b1 is simple
proof end;
end;

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

Lm9: 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 inducedSubgraph of G, the_Vertices_of G,E;
coherence
for b1 being inducedSubgraph of G, the_Vertices_of G,E holds b1 is spanning
proof end;
end;

registration
let G be _Graph;
cluster -> spanning inducedSubgraph of G, the_Vertices_of G, {} ;
coherence
for b1 being inducedSubgraph of G, the_Vertices_of G, {} holds b1 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 inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};
coherence
for b1 being removeEdge of G,e holds b1 is spanning ;
end;

registration
let G be _Graph;
let E be set ;
cluster -> spanning inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
coherence
for b1 being removeEdges of G,E holds b1 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 40
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 41
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 42
G .edgesInOut {v};
coherence
G .edgesInOut {v} is Subset of (the_Edges_of G) ;
end;

:: deftheorem defines .edgesIn() GLIB_000:def 40 :
for G being _Graph
for v being Vertex of G holds v .edgesIn() = G .edgesInto {v};

:: deftheorem defines .edgesOut() GLIB_000:def 41 :
for G being _Graph
for v being Vertex of G holds v .edgesOut() = G .edgesOutOf {v};

:: deftheorem defines .edgesInOut() GLIB_000:def 42 :
for G being _Graph
for v being Vertex of G holds v .edgesInOut() = G .edgesInOut {v};

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

Lm11: 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 set ;
func v .adj e -> Vertex of G equals :Def43: :: GLIB_000:def 43
(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:7;
consistency
for b1 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
( b1 = (the_Source_of G) . e iff b1 = (the_Target_of G) . e ) ;
end;

:: deftheorem Def43 defines .adj GLIB_000:def 43 :
for G being _Graph
for v being Vertex of G
for e being set holds
( ( e in the_Edges_of G & (the_Target_of G) . e = v implies v .adj e = (the_Source_of G) . e ) & ( e in the_Edges_of G & (the_Source_of G) . e = v & not (the_Target_of G) . e = v implies v .adj e = (the_Target_of G) . e ) & ( ( not e in the_Edges_of G or not (the_Target_of G) . e = v ) & ( not e in the_Edges_of G or not (the_Source_of G) . e = v or (the_Target_of G) . e = v ) implies v .adj e = v ) );

definition
let G be _Graph;
let v be Vertex of G;
func v .inDegree() -> Cardinal equals :: GLIB_000:def 44
 Card (v .edgesIn() );
coherence
Card (v .edgesIn() ) is Cardinal ;
func v .outDegree() -> Cardinal equals :: GLIB_000:def 45
 Card (v .edgesOut() );
coherence
Card (v .edgesOut() ) is Cardinal ;
end;

:: deftheorem defines .inDegree() GLIB_000:def 44 :
for G being _Graph
for v being Vertex of G holds v .inDegree() = Card (v .edgesIn() );

:: deftheorem defines .outDegree() GLIB_000:def 45 :
for G being _Graph
for v being Vertex of G holds v .outDegree() = Card (v .edgesOut() );

definition
let G be finite _Graph;
let v be Vertex of G;
:: original: .inDegree()
redefine func v .inDegree() -> Nat;
coherence
v .inDegree() is Nat
proof end;
:: original: .outDegree()
redefine func v .outDegree() -> Nat;
coherence
v .outDegree() is Nat
proof end;
end;

definition
let G be _Graph;
let v be Vertex of G;
func v .degree() -> Cardinal equals :: GLIB_000:def 46
(v .inDegree() ) +` (v .outDegree() );
coherence
(v .inDegree() ) +` (v .outDegree() ) is Cardinal ;
end;

:: deftheorem defines .degree() GLIB_000:def 46 :
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() -> Nat equals :: GLIB_000:def 47
(v .inDegree() ) + (v .outDegree() );
correctness
coherence
v .degree() is Nat;
compatibility
for b1 being Nat holds
( b1 = v .degree() iff b1 = (v .inDegree() ) + (v .outDegree() ) );
proof end;
end;

:: deftheorem defines .degree() GLIB_000:def 47 :
for G being finite _Graph
for v being Vertex of G holds v .degree() = (v .inDegree() ) + (v .outDegree() );

definition
let G be _Graph;
let v be Vertex of G;
func v .inNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 48
(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 49
(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 48 :
for G being _Graph
for v being Vertex of G holds v .inNeighbors() = (the_Source_of G) .: (v .edgesIn() );

:: deftheorem defines .outNeighbors() GLIB_000:def 49 :
for G being _Graph
for v being Vertex of G holds v .outNeighbors() = (the_Target_of G) .: (v .edgesOut() );

definition
let G be _Graph;
let v be Vertex of G;
func v .allNeighbors() -> Subset of (the_Vertices_of G) equals :: GLIB_000:def 50
(v .inNeighbors() ) \/ (v .outNeighbors() );
coherence
(v .inNeighbors() ) \/ (v .outNeighbors() ) is Subset of (the_Vertices_of G) ;
end;

:: deftheorem defines .allNeighbors() GLIB_000:def 50 :
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 :Def51: :: GLIB_000:def 51
v .edgesInOut() = {} ;
end;

:: deftheorem Def51 defines isolated GLIB_000:def 51 :
for G being _Graph
for v being Vertex of G holds
( v is isolated iff v .edgesInOut() = {} );

definition
let G be finite _Graph;
let v be Vertex of G;
redefine attr v is isolated means :: GLIB_000:def 52
v .degree() = 0;
compatibility
( v is isolated iff v .degree() = 0 )
proof end;
end;

:: deftheorem defines isolated GLIB_000:def 52 :
for G being finite _Graph
for v being Vertex of G holds
( v is isolated iff v .degree() = 0 );

definition
let G be _Graph;
let v be Vertex of G;
attr v is endvertex means :Def53: :: GLIB_000:def 53
 ex e being set st
( v .edgesInOut() = {e} & not e Joins v,v,G );
end;

:: deftheorem Def53 defines endvertex GLIB_000:def 53 :
for G being _Graph
for v being Vertex of G holds
( v is endvertex iff ex e being set st
( v .edgesInOut() = {e} & not e Joins v,v,G ) );

definition
let G be finite _Graph;
let v be Vertex of G;
redefine attr v is endvertex means :: GLIB_000:def 54
v .degree() = 1;
compatibility
( v is endvertex iff v .degree() = 1 )
proof end;
end;

:: deftheorem defines endvertex GLIB_000:def 54 :
for G being finite _Graph
for v being Vertex of G holds
( v is endvertex iff v .degree() = 1 );

definition
let F be ManySortedSet of NAT ;
attr F is Graph-yielding means :Def55: :: GLIB_000:def 55
for n being Nat holds F . n is _Graph;
attr F is halting means :Def56: :: GLIB_000:def 56
 ex n being Nat st F . n = F . (n + 1);
end;

:: deftheorem Def55 defines Graph-yielding GLIB_000:def 55 :
for F being ManySortedSet of NAT holds
( F is Graph-yielding iff for n being Nat holds F . n is _Graph );

:: deftheorem Def56 defines halting GLIB_000:def 56 :
for F being ManySortedSet of NAT holds
( F is halting iff ex n being Nat st F . n = F . (n + 1) );

definition
let F be ManySortedSet of NAT ;
func F .Lifespan() -> Nat means :: GLIB_000:def 57
( 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 b1 being Nat st
( F . b1 = F . (b1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b1 <= n ) ) ) & ( not F is halting implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( F is halting & F . b1 = F . (b1 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b1 <= n ) & F . b2 = F . (b2 + 1) & ( for n being Nat st F . n = F . (n + 1) holds
b2 <= n ) implies b1 = b2 ) & ( not F is halting & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum ;
end;

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

definition
let F be ManySortedSet of NAT ;
func F .Result() -> set equals :: GLIB_000:def 58
F . (F .Lifespan() );
coherence
F . (F .Lifespan() ) is set ;
end;

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

registration
cluster Graph-yielding ManySortedSet of NAT ;
existence
ex b1 being ManySortedSet of NAT st b1 is Graph-yielding
proof end;
end;

definition
mode GraphSeq is Graph-yielding ManySortedSet of NAT ;
end;

definition
let GSq be GraphSeq;
let x be Nat;
func GSq .-> x -> _Graph equals :: GLIB_000:def 59
GSq . x;
coherence
GSq . x is _Graph by Def55;
end;

:: deftheorem defines .-> GLIB_000:def 59 :
for GSq being GraphSeq
for x being Nat holds GSq .-> x = GSq . x;

definition
let GSq be GraphSeq;
attr GSq is finite means :Def60: :: GLIB_000:def 60
for x being Nat holds GSq .-> x is finite;
attr GSq is loopless means :Def61: :: GLIB_000:def 61
for x being Nat holds GSq .-> x is loopless;
attr GSq is trivial means :Def62: :: GLIB_000:def 62
for x being Nat holds GSq .-> x is trivial;
attr GSq is non-trivial means :Def63: :: GLIB_000:def 63
for x being Nat holds not GSq .-> x is trivial;
attr GSq is non-multi means :Def64: :: GLIB_000:def 64
for x being Nat holds GSq .-> x is non-multi;
attr GSq is non-Dmulti means :Def65: :: GLIB_000:def 65
for x being Nat holds GSq .-> x is non-Dmulti;
attr GSq is simple means :Def66: :: GLIB_000:def 66
for x being Nat holds GSq .-> x is simple;
attr GSq is Dsimple means :Def67: :: GLIB_000:def 67
for x being Nat holds GSq .-> x is Dsimple;
end;

:: deftheorem Def60 defines finite GLIB_000:def 60 :
for GSq being GraphSeq holds
( GSq is finite iff for x being Nat holds GSq .-> x is finite );

:: deftheorem Def61 defines loopless GLIB_000:def 61 :
for GSq being GraphSeq holds
( GSq is loopless iff for x being Nat holds GSq .-> x is loopless );

:: deftheorem Def62 defines trivial GLIB_000:def 62 :
for GSq being GraphSeq holds
( GSq is trivial iff for x being Nat holds GSq .-> x is trivial );

:: deftheorem Def63 defines non-trivial GLIB_000:def 63 :
for GSq being GraphSeq holds
( GSq is non-trivial iff for x being Nat holds not GSq .-> x is trivial );

:: deftheorem Def64 defines non-multi GLIB_000:def 64 :
for GSq being GraphSeq holds
( GSq is non-multi iff for x being Nat holds GSq .-> x is non-multi );

:: deftheorem Def65 defines non-Dmulti GLIB_000:def 65 :
for GSq being GraphSeq holds
( GSq is non-Dmulti iff for x being Nat holds GSq .-> x is non-Dmulti );

:: deftheorem Def66 defines simple GLIB_000:def 66 :
for GSq being GraphSeq holds
( GSq is simple iff for x being Nat holds GSq .-> x is simple );

:: deftheorem Def67 defines Dsimple GLIB_000:def 67 :
for GSq being GraphSeq holds
( GSq is Dsimple iff for x being Nat holds GSq .-> x is Dsimple );

definition
let GSq be GraphSeq;
redefine attr GSq is halting means :: GLIB_000:def 68
 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) )
proof end;
end;

:: deftheorem defines halting GLIB_000:def 68 :
for GSq being GraphSeq holds
( GSq is halting iff ex n being Nat st GSq .-> n = GSq .-> (n + 1) );

registration
cluster halting finite loopless trivial non-multi non-Dmulti simple Dsimple ManySortedSet of NAT ;
existence
ex b1 being GraphSeq st
( b1 is halting & b1 is finite & b1 is loopless & b1 is trivial & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple )
proof end;
cluster halting finite loopless non-trivial non-multi non-Dmulti simple Dsimple ManySortedSet of NAT ;
existence
ex b1 being GraphSeq st
( b1 is halting & b1 is finite & b1 is loopless & b1 is non-trivial & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple )
proof end;
end;

registration
let GSq be finite GraphSeq;
let x be Nat;
cluster GSq .-> x -> finite ;
coherence
GSq .-> x is finite by Def60;
end;

registration
let GSq be loopless GraphSeq;
let x be Nat;
cluster GSq .-> x -> loopless ;
coherence
GSq .-> x is loopless by Def61;
end;

registration
let GSq be trivial GraphSeq;
let x be Nat;
cluster GSq .-> x -> trivial ;
coherence
GSq .-> x is trivial by Def62;
end;

registration
let GSq be non-trivial GraphSeq;
let x be Nat;
cluster GSq .-> x -> non trivial ;
coherence
not GSq .-> x is trivial by Def63;
end;

registration
let GSq be non-multi GraphSeq;
let x be Nat;
cluster GSq .-> x -> non-multi non-Dmulti ;
coherence
GSq .-> x is non-multi by Def64;
end;

registration
let GSq be non-Dmulti GraphSeq;
let x be Nat;
cluster GSq .-> x -> non-Dmulti ;
coherence
GSq .-> x is non-Dmulti by Def65;
end;

registration
let GSq be simple GraphSeq;
let x be Nat;
cluster GSq .-> x -> loopless non-multi non-Dmulti simple Dsimple ;
coherence
GSq .-> x is simple by Def66;
end;

registration
let GSq be Dsimple GraphSeq;
let x be Nat;
cluster GSq .-> x -> loopless non-Dmulti Dsimple ;
coherence
GSq .-> x is Dsimple by Def67;
end;

registration
cluster non-multi -> non-Dmulti ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is non-multi holds
b1 is non-Dmulti
proof end;
end;

registration
cluster simple -> loopless non-multi non-Dmulti ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is simple holds
( b1 is loopless & b1 is non-multi )
proof end;
end;

registration
cluster loopless non-multi -> loopless non-multi non-Dmulti simple ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is loopless & b1 is non-multi holds
b1 is simple
proof end;
end;

registration
cluster loopless non-Dmulti -> Dsimple ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is loopless & b1 is non-Dmulti holds
b1 is Dsimple
proof end;
end;

registration
cluster Dsimple -> loopless non-Dmulti Dsimple ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is Dsimple holds
( b1 is loopless & b1 is non-Dmulti )
proof end;
end;

registration
cluster loopless trivial -> finite ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is trivial & b1 is loopless holds
b1 is finite
proof end;
end;

registration
cluster trivial non-Dmulti -> finite ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is trivial & b1 is non-Dmulti holds
b1 is finite
proof end;
end;

theorem :: GLIB_000:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 & TargetSelector = 4 ) ;

theorem :: GLIB_000:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds
( x in _GraphSelectors iff ( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector ) ) by ENUMSET1:def 2;

theorem :: GLIB_000:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds _GraphSelectors c= dom G
proof end;

theorem :: GLIB_000:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm1;

theorem :: GLIB_000:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GLIB_000:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm3;

theorem :: GLIB_000:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm2;

theorem Th9: :: GLIB_000:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GS being GraphStruct
for x being set
for n being Nat holds dom (GS .set n,x) = (dom GS) \/ {n}
proof end;

theorem :: GLIB_000:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GS being GraphStruct
for x being set
for n being Nat holds dom GS c= dom (GS .set n,x) by FUNCT_4:11;

theorem Th11: :: GLIB_000:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for GS being GraphStruct
for x being set
for n being Nat holds (GS .set n,x) . n = x
proof end;

theorem Th12: :: GLIB_000:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th11;

theorem :: GLIB_000:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x, y being set st e Joins x,y,G holds
( x in the_Vertices_of G & y in the_Vertices_of G )
proof end;

theorem :: GLIB_000:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x, y being set st e Joins x,y,G holds
e Joins y,x,G
proof end;

theorem :: GLIB_000:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x1, y1, x2, y2 being set st e Joins x1,y1,G & e Joins x2,y2,G & not ( x1 = x2 & y1 = y2 ) holds
( x1 = y2 & y1 = x2 )
proof end;

theorem :: GLIB_000:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) ) by Lm4;

theorem :: GLIB_000:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x, y, X, Y being set 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
proof end;

theorem :: GLIB_000:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds
( G is loopless iff for v, e being set holds not e Joins v,v,G )
proof end;

theorem :: GLIB_000:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite loopless _Graph
for v being Vertex of G holds v .degree() = card (v .edgesInOut() )
proof end;

theorem :: GLIB_000:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non trivial _Graph ex v1, v2 being Vertex of G st v1 <> v2
proof end;

theorem Th25: :: GLIB_000:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being trivial _Graph ex v being Vertex of G st the_Vertices_of G = {v}
proof end;

theorem :: GLIB_000:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being loopless trivial _Graph holds the_Edges_of G = {}
proof end;

theorem :: GLIB_000:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph st the_Edges_of G = {} holds
G is simple
proof end;

theorem :: GLIB_000:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph holds G .order() >= 1
proof end;

theorem :: GLIB_000:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph holds
( G .order() = 1 iff G is trivial ) by Def21, CARD_2:20;

theorem :: GLIB_000:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph holds
( G .order() = 1 iff ex v being Vertex of G st the_Vertices_of G = {v} )
proof end;

theorem Th31: :: GLIB_000:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for X being set holds
( G .edgesInto X c= G .edgesInOut X & G .edgesOutOf X c= G .edgesInOut X )
proof end;

theorem :: GLIB_000:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds the_Edges_of G = G .edgesInOut (the_Vertices_of G)
proof end;

theorem :: GLIB_000:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm8;

theorem :: GLIB_000:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x, X, y, e being set st x in X & y in X & e Joins x,y,G holds
e in G .edgesBetween X
proof end;

theorem :: GLIB_000:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for X being set holds G .edgesBetween X c= G .edgesInOut X
proof end;

theorem Th37: :: GLIB_000:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G)
proof end;

theorem Th38: :: GLIB_000:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds G is Subgraph of G by Lm6;

theorem Th44: :: GLIB_000:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th46: :: GLIB_000:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th47: :: GLIB_000:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th48: :: GLIB_000:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th50: :: GLIB_000:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th52: :: GLIB_000:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th54: :: GLIB_000:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th56: :: GLIB_000:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being finite _Graph
for E being set
for G2 being removeEdges of G1,E holds G1 .order() = G2 .order() by Th56;

theorem :: GLIB_000:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm10;

theorem :: GLIB_000:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm11;

theorem :: GLIB_000:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for v being Vertex of G holds v .edgesInOut() = (v .edgesIn() ) \/ (v .edgesOut() ) ;

theorem Th64: :: GLIB_000:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th65: :: GLIB_000:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x being set
for v1 being Vertex of G st e Joins v1,x,G holds
e in v1 .edgesInOut()
proof end;

theorem Th66: :: GLIB_000:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e, x, y being set
for v being Vertex of G st e in v .edgesInOut() & e Joins x,y,G & not v = x holds
v = y
proof end;

theorem :: GLIB_000:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for e being set
for v1, v2 being Vertex of G st e Joins v1,v2,G holds
( v1 .adj e = v2 & v2 .adj e = v1 )
proof end;

theorem :: GLIB_000:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th72: :: GLIB_000:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .inNeighbors() iff ex e being set st e DJoins x,v,G )
proof end;

theorem Th73: :: GLIB_000:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .outNeighbors() iff ex e being set st e DJoins v,x,G )
proof end;

theorem Th74: :: GLIB_000:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x being set
for v being Vertex of G holds
( x in v .allNeighbors() iff ex e being set st e Joins v,x,G )
proof end;

theorem Th75: :: GLIB_000:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
proof end;

theorem :: GLIB_000:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: GLIB_000:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th81: :: GLIB_000:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th82: :: GLIB_000:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th88: :: GLIB_000:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2, G3 being _Graph st G1 == G2 & G2 == G3 holds
G1 == G3
proof end;

theorem Th89: :: GLIB_000:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th90: :: GLIB_000:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph holds
( G1 == G2 iff ( G1 is Subgraph of G2 & G2 is Subgraph of G1 ) )
proof end;

theorem Th91: :: GLIB_000:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for e, x, y, X, Y being set st G1 == G2 holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e SJoins X,Y,G1 implies e SJoins X,Y,G2 ) & ( e DSJoins X,Y,G1 implies e DSJoins X,Y,G2 ) )
proof end;

theorem :: GLIB_000:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th93: :: GLIB_000:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th94: :: GLIB_000:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for V, E being set
for G1, G2 being inducedSubgraph of G,V,E holds G1 == G2
proof end;

theorem :: GLIB_000:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being inducedSubgraph of G1,(the_Vertices_of G1) holds G1 == G2
proof end;

theorem :: GLIB_000:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th99: :: GLIB_000:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th101: :: GLIB_000:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for G1, G2 being Subgraph of G holds
( not G1 c< G2 or ex v being set st
( v in the_Vertices_of G2 & not v in the_Vertices_of G1 ) or ex e being set st
( e in the_Edges_of G2 & not e in the_Edges_of G1 ) )
proof end;