:: GLIB_000 semantic presentation

definition

mode GraphStruct -> finite Function means :Def1: :: GLIB_000:def 1
dom a₁ c= NAT ;
existence

proof end;

end;

:: deftheorem Def1 defines GraphStruct GLIB_000:def 1 :

definition

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

end;

:: deftheorem Def2 defines VertexSelector GLIB_000:def 2 :

:: deftheorem Def3 defines EdgeSelector GLIB_000:def 3 :

:: deftheorem Def4 defines SourceSelector GLIB_000:def 4 :

:: deftheorem Def5 defines TargetSelector GLIB_000:def 5 :

definition

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

end;

:: deftheorem Def6 defines _GraphSelectors GLIB_000:def 6 :

definition

let c₁ be GraphStruct ;
func the_Vertices_of c₁ -> set equals :: GLIB_000:def 7
a₁ . VertexSelector ;
coherence ;
func the_Edges_of c₁ -> set equals :: GLIB_000:def 8
a₁ . EdgeSelector ;
coherence ;
func the_Source_of c₁ -> set equals :: GLIB_000:def 9
a₁ . SourceSelector ;
coherence ;
func the_Target_of c₁ -> set equals :: GLIB_000:def 10
a₁ . TargetSelector ;
coherence ;

end;

:: deftheorem Def7 defines the_Vertices_of GLIB_000:def 7 :

:: deftheorem Def8 defines the_Edges_of GLIB_000:def 8 :

:: deftheorem Def9 defines the_Source_of GLIB_000:def 9 :

:: deftheorem Def10 defines the_Target_of GLIB_000:def 10 :

definition

let c₁ be GraphStruct ;
attr a₁ is [Graph-like] means :Def11: :: GLIB_000:def 11
( VertexSelector in dom a₁ & EdgeSelector in dom a₁ & SourceSelector in dom a₁ & TargetSelector in dom a₁ & the_Vertices_of a₁ is non empty set & the_Source_of a₁ is Function of the_Edges_of a₁, the_Vertices_of a₁ & the_Target_of a₁ is Function of the_Edges_of a₁, the_Vertices_of a₁ );

end;

:: deftheorem Def11 defines [Graph-like] GLIB_000:def 11 :

registration

cluster finite [Graph-like] GraphStruct ;
existence

proof end;

end;

definition

mode _Graph is [Graph-like] GraphStruct ;

end;

registration

let c₁ be _Graph;
cluster the_Vertices_of a₁ -> non empty ;
coherence by Def11;

end;

definition

let c₁ be _Graph;
redefine func the_Source_of as the_Source_of c₁ -> Function of the_Edges_of a₁, the_Vertices_of a₁;
coherence by Def11;
redefine func the_Target_of as the_Target_of c₁ -> Function of the_Edges_of a₁, the_Vertices_of a₁;
coherence by Def11;

end;

Lemma3: for b₁ being _Graph holds
( dom (the_Source_of b₁) = the_Edges_of b₁ & dom (the_Target_of b₁) = the_Edges_of b₁ & rng (the_Source_of b₁) c= the_Vertices_of b₁ & rng (the_Target_of b₁) c= the_Vertices_of b₁ )
by FUNCT_2:def 1;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃, c₄ be Function of c₂,c₁;
func createGraph c₁,c₂,c₃,c₄ -> _Graph equals :: GLIB_000:def 12
<*a₁,a₂,a₃,a₄*>;
coherence

proof end;

end;

:: deftheorem Def12 defines createGraph GLIB_000:def 12 :

Lemma4: for b₁ being non empty set
for b₂ being set
for b₃, b₄ being Function of b₂,b₁ holds
( the_Vertices_of (createGraph b₁,b₂,b₃,b₄) = b₁ & the_Edges_of (createGraph b₁,b₂,b₃,b₄) = b₂ & the_Source_of (createGraph b₁,b₂,b₃,b₄) = b₃ & the_Target_of (createGraph b₁,b₂,b₃,b₄) = b₄ )
by SCMPDS_1:3;

registration

let c₁, c₂ be set ;
cluster a₁ .--> a₂ -> finite ;
coherence

proof end;

end;

definition

let c₁ be GraphStruct ;
let c₂ be Nat;
let c₃ be set ;
func c₁ .set c₂,c₃ -> GraphStruct equals :: GLIB_000:def 13
a₁ +* (a₂ .--> a₃);
coherence

proof end;

end;

:: deftheorem Def13 defines .set GLIB_000:def 13 :

definition

let c₁ be GraphStruct ;
let c₂ be set ;
func c₁ .strict c₂ -> GraphStruct equals :: GLIB_000:def 14
a₁ | a₂;
coherence

proof end;

end;

:: deftheorem Def14 defines .strict GLIB_000:def 14 :

Lemma5: for b₁ being GraphStruct holds
( b₁ is [Graph-like] iff ( _GraphSelectors c= dom b₁ & not the_Vertices_of b₁ is empty & the_Source_of b₁ is Function of the_Edges_of b₁, the_Vertices_of b₁ & the_Target_of b₁ is Function of the_Edges_of b₁, the_Vertices_of b₁ ) )

proof end;

registration

let c₁ be _Graph;
cluster a₁ .strict _GraphSelectors -> finite [Graph-like] ;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂, c₃, c₄ be set ;
pred c₄ Joins c₂,c₃,c₁ means :Def15: :: GLIB_000:def 15
( a₄ in the_Edges_of a₁ & ( ( (the_Source_of a₁) . a₄ = a₂ & (the_Target_of a₁) . a₄ = a₃ ) or ( (the_Source_of a₁) . a₄ = a₃ & (the_Target_of a₁) . a₄ = a₂ ) ) );

end;

:: deftheorem Def15 defines Joins GLIB_000:def 15 :

definition

let c₁ be _Graph;
let c₂, c₃, c₄ be set ;
pred c₄ DJoins c₂,c₃,c₁ means :Def16: :: GLIB_000:def 16
( a₄ in the_Edges_of a₁ & (the_Source_of a₁) . a₄ = a₂ & (the_Target_of a₁) . a₄ = a₃ );

end;

:: deftheorem Def16 defines DJoins GLIB_000:def 16 :

definition

let c₁ be _Graph;
let c₂, c₃, c₄ be set ;
pred c₄ SJoins c₂,c₃,c₁ means :Def17: :: GLIB_000:def 17
( a₄ in the_Edges_of a₁ & ( ( (the_Source_of a₁) . a₄ in a₂ & (the_Target_of a₁) . a₄ in a₃ ) or ( (the_Source_of a₁) . a₄ in a₃ & (the_Target_of a₁) . a₄ in a₂ ) ) );
pred c₄ DSJoins c₂,c₃,c₁ means :Def18: :: GLIB_000:def 18
( a₄ in the_Edges_of a₁ & (the_Source_of a₁) . a₄ in a₂ & (the_Target_of a₁) . a₄ in a₃ );

end;

:: deftheorem Def17 defines SJoins GLIB_000:def 17 :

:: deftheorem Def18 defines DSJoins GLIB_000:def 18 :

Lemma10: for b₁ being _Graph
for b₂, b₃, b₄ being set holds
( b₂ Joins b₃,b₄,b₁ iff ( b₂ DJoins b₃,b₄,b₁ or b₂ DJoins b₄,b₃,b₁ ) )

proof end;

definition

let c₁ be _Graph;
attr a₁ is finite means :Def19: :: GLIB_000:def 19
( the_Vertices_of a₁ is finite & the_Edges_of a₁ is finite );
attr a₁ is loopless means :Def20: :: GLIB_000:def 20
for b₁ being set holds
( not b₁ in the_Edges_of a₁ or not (the_Source_of a₁) . b₁ = (the_Target_of a₁) . b₁ );
attr a₁ is trivial means :Def21: :: GLIB_000:def 21
Card (the_Vertices_of a₁) = one ;
attr a₁ is non-multi means :Def22: :: GLIB_000:def 22
for b₁, b₂, b₃, b₄ being set st b₁ Joins b₃,b₄,a₁ & b₂ Joins b₃,b₄,a₁ holds
b₁ = b₂;
attr a₁ is non-Dmulti means :Def23: :: GLIB_000:def 23
for b₁, b₂, b₃, b₄ being set st b₁ DJoins b₃,b₄,a₁ & b₂ DJoins b₃,b₄,a₁ holds
b₁ = b₂;

end;

:: deftheorem Def19 defines finite GLIB_000:def 19 :

:: deftheorem Def20 defines loopless GLIB_000:def 20 :

:: deftheorem Def21 defines trivial GLIB_000:def 21 :

:: deftheorem Def22 defines non-multi GLIB_000:def 22 :

:: deftheorem Def23 defines non-Dmulti GLIB_000:def 23 :

definition

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

end;

:: deftheorem Def24 defines simple GLIB_000:def 24 :

:: deftheorem Def25 defines Dsimple GLIB_000:def 25 :

Lemma18: for b₁ being _Graph st the_Edges_of b₁ = {} holds
b₁ is simple

proof end;

registration

cluster non-multi -> non-Dmulti GraphStruct ;
coherence

proof end;

cluster simple -> loopless non-multi GraphStruct ;
coherence by Def24;
cluster loopless non-multi -> simple GraphStruct ;
coherence by Def24;
cluster loopless non-Dmulti -> Dsimple GraphStruct ;
coherence by Def25;
cluster Dsimple -> loopless non-Dmulti GraphStruct ;
coherence by Def25;
cluster loopless trivial -> finite GraphStruct ;
coherence

proof end;

cluster trivial non-Dmulti -> finite GraphStruct ;
coherence

proof end;

end;

registration

cluster finite loopless trivial non-multi non-Dmulti simple Dsimple GraphStruct ;
existence

proof end;

cluster finite loopless non trivial non-multi non-Dmulti simple Dsimple GraphStruct ;
existence

proof end;

end;

registration

let c₁ be finite _Graph;
cluster the_Vertices_of a₁ -> non empty finite ;
coherence by Def19;
cluster the_Edges_of a₁ -> finite ;
coherence by Def19;

end;

registration

let c₁ be trivial _Graph;
cluster the_Vertices_of a₁ -> non empty finite ;
coherence

proof end;

end;

registration

let c₁ be non empty finite set ;
let c₂ be finite set ;
let c₃, c₄ be Function of c₂,c₁;
cluster createGraph a₁,a₂,a₃,a₄ -> finite ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be empty set ;
let c₃, c₄ be Function of c₂,c₁;
cluster createGraph a₁,a₂,a₃,a₄ -> loopless non-multi non-Dmulti simple Dsimple ;
coherence

proof end;

end;

registration

let c₁, c₂ be set ;
let c₃, c₄ be Function of c₂,{c₁};
cluster createGraph {a₁},a₂,a₃,a₄ -> trivial ;
coherence

proof end;

end;

definition

let c₁ be _Graph;
func c₁ .order() -> Cardinal equals :: GLIB_000:def 26
Card (the_Vertices_of a₁);
coherence ;

end;

:: deftheorem Def26 defines .order() GLIB_000:def 26 :

definition

let c₁ be finite _Graph;
redefine func .order() as c₁ .order() -> non empty Nat;
coherence

proof end;

end;

definition

let c₁ be _Graph;
func c₁ .size() -> Cardinal equals :: GLIB_000:def 27
Card (the_Edges_of a₁);
coherence ;

end;

:: deftheorem Def27 defines .size() GLIB_000:def 27 :

definition

let c₁ be finite _Graph;
redefine func .size() as c₁ .size() -> Nat;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be set ;
func c₁ .edgesInto c₂ -> Subset of (the_Edges_of a₁) means :Def28: :: GLIB_000:def 28
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in the_Edges_of a₁ & (the_Target_of a₁) . b₁ in a₂ ) );
existence

proof end;

uniqueness

proof end;

func c₁ .edgesOutOf c₂ -> Subset of (the_Edges_of a₁) means :Def29: :: GLIB_000:def 29
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in the_Edges_of a₁ & (the_Source_of a₁) . b₁ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines .edgesInto GLIB_000:def 28 :

:: deftheorem Def29 defines .edgesOutOf GLIB_000:def 29 :

definition

let c₁ be _Graph;
let c₂ be set ;
func c₁ .edgesInOut c₂ -> Subset of (the_Edges_of a₁) equals :: GLIB_000:def 30
(a₁ .edgesInto a₂) \/ (a₁ .edgesOutOf a₂);
coherence ;
func c₁ .edgesBetween c₂ -> Subset of (the_Edges_of a₁) equals :: GLIB_000:def 31
(a₁ .edgesInto a₂) /\ (a₁ .edgesOutOf a₂);
coherence ;

end;

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

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

definition

let c₁ be _Graph;
let c₂, c₃ be set ;
func c₁ .edgesBetween c₂,c₃ -> Subset of (the_Edges_of a₁) means :Def32: :: GLIB_000:def 32
for b₁ being set holds
( b₁ in a₄ iff b₁ SJoins a₂,a₃,a₁ );
existence

proof end;

uniqueness

proof end;

func c₁ .edgesDBetween c₂,c₃ -> Subset of (the_Edges_of a₁) means :Def33: :: GLIB_000:def 33
for b₁ being set holds
( b₁ in a₄ iff b₁ DSJoins a₂,a₃,a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines .edgesBetween GLIB_000:def 32 :

:: deftheorem Def33 defines .edgesDBetween GLIB_000:def 33 :

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

for b₁ being finite _Graph holds P₁[b₁]

provided

E23: for b₁ being finite _Graph st b₁ .order() = 1 holds
P₁[b₁] and
E24: for b₁ being non empty Nat st ( for b₂ being finite _Graph st b₂ .order() = b₁ holds
P₁[b₂] ) holds
for b₂ being finite _Graph st b₂ .order() = b₁ + 1 holds
P₁[b₂]

proof end;

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

for b₁ being finite _Graph holds P₁[b₁]

provided

E23: for b₁ being finite _Graph st b₁ .size() = 0 holds
P₁[b₁] and
E24: for b₁ being Nat st ( for b₂ being finite _Graph st b₂ .size() = b₁ holds
P₁[b₂] ) holds
for b₂ being finite _Graph st b₂ .size() = b₁ + 1 holds
P₁[b₂]

proof end;

definition

let c₁ be _Graph;
mode Subgraph of c₁ -> _Graph means :Def34: :: GLIB_000:def 34
( the_Vertices_of a₂ c= the_Vertices_of a₁ & the_Edges_of a₂ c= the_Edges_of a₁ & ( for b₁ being set st b₁ in the_Edges_of a₂ holds
( (the_Source_of a₂) . b₁ = (the_Source_of a₁) . b₁ & (the_Target_of a₂) . b₁ = (the_Target_of a₁) . b₁ ) ) );
existence

proof end;

end;

:: deftheorem Def34 defines Subgraph GLIB_000:def 34 :

definition

let c₁ be _Graph;
let c₂ be Subgraph of c₁;
redefine func the_Vertices_of as the_Vertices_of c₂ -> non empty Subset of (the_Vertices_of a₁);
coherence by Def34;
redefine func the_Edges_of as the_Edges_of c₂ -> Subset of (the_Edges_of a₁);
coherence by Def34;

end;

registration

let c₁ be _Graph;
cluster finite loopless trivial non-multi non-Dmulti simple Dsimple Subgraph of a₁;
existence

proof end;

end;

Lemma24: for b₁ being _Graph holds b₁ is Subgraph of b₁

proof end;

Lemma25: for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃, b₄, b₅ being set st b₅ Joins b₃,b₄,b₂ holds
b₅ Joins b₃,b₄,b₁

proof end;

registration

let c₁ be finite _Graph;
cluster -> finite Subgraph of a₁;
coherence

proof end;

end;

registration

let c₁ be loopless _Graph;
cluster -> loopless Subgraph of a₁;
coherence

proof end;

end;

registration

let c₁ be trivial _Graph;
cluster -> trivial Subgraph of a₁;
coherence

proof end;

end;

registration

let c₁ be non-multi _Graph;
cluster -> non-multi Subgraph of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Subgraph of c₁;
attr a₂ is spanning means :Def35: :: GLIB_000:def 35
the_Vertices_of a₂ = the_Vertices_of a₁;

end;

:: deftheorem Def35 defines spanning GLIB_000:def 35 :

registration

let c₁ be _Graph;
cluster spanning Subgraph of a₁;
existence

proof end;

end;

definition

let c₁, c₂ be _Graph;
pred c₁ == c₂ means :Def36: :: GLIB_000:def 36
( the_Vertices_of a₁ = the_Vertices_of a₂ & the_Edges_of a₁ = the_Edges_of a₂ & the_Source_of a₁ = the_Source_of a₂ & the_Target_of a₁ = the_Target_of a₂ );
reflexivity ;
symmetry ;

end;

:: deftheorem Def36 defines == GLIB_000:def 36 :

notation

let c₁, c₂ be _Graph;
antonym c₁ != c₂ for c₁ == c₂;

end;

definition

let c₁, c₂ be _Graph;
pred c₁ c= c₂ means :Def37: :: GLIB_000:def 37
a₁ is Subgraph of a₂;
reflexivity by Lemma24;

end;

:: deftheorem Def37 defines c= GLIB_000:def 37 :

definition

let c₁, c₂ be _Graph;
pred c₁ c< c₂ means :Def38: :: GLIB_000:def 38
( a₁ c= a₂ & a₁ != a₂ );
irreflexivity ;

end;

:: deftheorem Def38 defines c< GLIB_000:def 38 :

definition

let c₁ be _Graph;
let c₂, c₃ be set ;
mode inducedSubgraph of c₁,c₂,c₃ -> Subgraph of a₁ means :Def39: :: GLIB_000:def 39
( the_Vertices_of a₄ = a₂ & the_Edges_of a₄ = a₃ ) if ( a₂ is non empty Subset of (the_Vertices_of a₁) & a₃ c= a₁ .edgesBetween a₂ )
otherwise a₄ == a₁;
existence

proof end;

consistency ;

end;

:: deftheorem Def39 defines inducedSubgraph GLIB_000:def 39 :

definition

let c₁ be _Graph;
let c₂ be set ;
mode inducedSubgraph of a₁,a₂ is inducedSubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

registration

let c₁ be _Graph;
let c₂ be non empty finite Subset of (the_Vertices_of c₁);
let c₃ be finite Subset of (c₁ .edgesBetween c₂);
cluster -> finite inducedSubgraph of a₁,a₂,a₃;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Element of the_Vertices_of c₁;
let c₃ be Subset of (c₁ .edgesBetween {c₂});
cluster -> trivial inducedSubgraph of a₁,{a₂},a₃;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Element of the_Vertices_of c₁;
cluster -> finite trivial inducedSubgraph of a₁,{a₂}, {} ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be non empty Subset of (the_Vertices_of c₁);
cluster -> simple inducedSubgraph of a₁,a₂, {} ;
coherence

proof end;

end;

Lemma31: for b₁ being _Graph
for b₂, b₃ being set holds
( ( b₂ in the_Edges_of b₁ & (the_Source_of b₁) . b₂ in b₃ & (the_Target_of b₁) . b₂ in b₃ ) iff b₂ in b₁ .edgesBetween b₃ )

proof end;

Lemma32: for b₁ being _Graph holds the_Edges_of b₁ = b₁ .edgesBetween (the_Vertices_of b₁)

proof end;

registration

let c₁ be _Graph;
let c₂ be Subset of (the_Edges_of c₁);
cluster -> spanning inducedSubgraph of a₁, the_Vertices_of a₁,a₂;
coherence

proof end;

end;

registration

let c₁ be _Graph;
cluster -> spanning inducedSubgraph of a₁, the_Vertices_of a₁, {} ;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be set ;
mode removeVertex of a₁,a₂ is inducedSubgraph of a₁,((the_Vertices_of a₁) \ {a₂});

end;

definition

let c₁ be _Graph;
let c₂ be set ;
mode removeVertices of a₁,a₂ is inducedSubgraph of a₁,((the_Vertices_of a₁) \ a₂);

end;

definition

let c₁ be _Graph;
let c₂ be set ;
mode removeEdge of a₁,a₂ is inducedSubgraph of a₁, the_Vertices_of a₁,(the_Edges_of a₁) \ {a₂};

end;

definition

let c₁ be _Graph;
let c₂ be set ;
mode removeEdges of a₁,a₂ is inducedSubgraph of a₁, the_Vertices_of a₁,(the_Edges_of a₁) \ a₂;

end;

registration

let c₁ be _Graph;
let c₂ be set ;
cluster -> spanning inducedSubgraph of a₁, the_Vertices_of a₁,(the_Edges_of a₁) \ {a₂};
coherence ;

end;

registration

let c₁ be _Graph;
let c₂ be set ;
cluster -> spanning inducedSubgraph of a₁, the_Vertices_of a₁,(the_Edges_of a₁) \ a₂;
coherence ;

end;

definition

let c₁ be _Graph;
mode Vertex of a₁ is Element of the_Vertices_of a₁;

end;

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₂ .edgesIn() -> Subset of (the_Edges_of a₁) equals :: GLIB_000:def 40
a₁ .edgesInto {a₂};
coherence ;
func c₂ .edgesOut() -> Subset of (the_Edges_of a₁) equals :: GLIB_000:def 41
a₁ .edgesOutOf {a₂};
coherence ;
func c₂ .edgesInOut() -> Subset of (the_Edges_of a₁) equals :: GLIB_000:def 42
a₁ .edgesInOut {a₂};
coherence ;

end;

:: deftheorem Def40 defines .edgesIn() GLIB_000:def 40 :

:: deftheorem Def41 defines .edgesOut() GLIB_000:def 41 :

:: deftheorem Def42 defines .edgesInOut() GLIB_000:def 42 :

Lemma33: for b₁ being _Graph
for b₂ being Vertex of b₁
for b₃ being set holds
( b₃ in b₂ .edgesIn() iff ( b₃ in the_Edges_of b₁ & (the_Target_of b₁) . b₃ = b₂ ) )

proof end;

Lemma34: for b₁ being _Graph
for b₂ being Vertex of b₁
for b₃ being set holds
( b₃ in b₂ .edgesOut() iff ( b₃ in the_Edges_of b₁ & (the_Source_of b₁) . b₃ = b₂ ) )

proof end;

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
let c₃ be set ;
func c₂ .adj c₃ -> Vertex of a₁ equals :Def43: :: GLIB_000:def 43
(the_Source_of a₁) . a₃ if ( a₃ in the_Edges_of a₁ & (the_Target_of a₁) . a₃ = a₂ )
(the_Target_of a₁) . a₃ if ( a₃ in the_Edges_of a₁ & (the_Source_of a₁) . a₃ = a₂ & not (the_Target_of a₁) . a₃ = a₂ )
otherwise a₂;
coherence by FUNCT_2:7;
consistency ;

end;

:: deftheorem Def43 defines .adj GLIB_000:def 43 :

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₂ .inDegree() -> Cardinal equals :: GLIB_000:def 44
Card (a₂ .edgesIn() );
coherence ;
func c₂ .outDegree() -> Cardinal equals :: GLIB_000:def 45
Card (a₂ .edgesOut() );
coherence ;

end;

:: deftheorem Def44 defines .inDegree() GLIB_000:def 44 :

:: deftheorem Def45 defines .outDegree() GLIB_000:def 45 :

definition

let c₁ be finite _Graph;
let c₂ be Vertex of c₁;
redefine func .inDegree() as c₂ .inDegree() -> Nat;
coherence

proof end;

redefine func .outDegree() as c₂ .outDegree() -> Nat;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₂ .degree() -> Cardinal equals :: GLIB_000:def 46
(a₂ .inDegree() ) +` (a₂ .outDegree() );
coherence ;

end;

:: deftheorem Def46 defines .degree() GLIB_000:def 46 :

definition

let c₁ be finite _Graph;
let c₂ be Vertex of c₁;
redefine func .degree() as c₂ .degree() -> Nat equals :: GLIB_000:def 47
(a₂ .inDegree() ) + (a₂ .outDegree() );
correctness

proof end;

end;

:: deftheorem Def47 defines .degree() GLIB_000:def 47 :

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₂ .inNeighbors() -> Subset of (the_Vertices_of a₁) equals :: GLIB_000:def 48
(the_Source_of a₁) .: (a₂ .edgesIn() );
coherence ;
func c₂ .outNeighbors() -> Subset of (the_Vertices_of a₁) equals :: GLIB_000:def 49
(the_Target_of a₁) .: (a₂ .edgesOut() );
coherence ;

end;

:: deftheorem Def48 defines .inNeighbors() GLIB_000:def 48 :

:: deftheorem Def49 defines .outNeighbors() GLIB_000:def 49 :

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₂ .allNeighbors() -> Subset of (the_Vertices_of a₁) equals :: GLIB_000:def 50
(a₂ .inNeighbors() ) \/ (a₂ .outNeighbors() );
coherence ;

end;

:: deftheorem Def50 defines .allNeighbors() GLIB_000:def 50 :

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
attr a₂ is isolated means :Def51: :: GLIB_000:def 51
a₂ .edgesInOut() = {} ;

end;

:: deftheorem Def51 defines isolated GLIB_000:def 51 :

definition

let c₁ be finite _Graph;
let c₂ be Vertex of c₁;
redefine attr a₂ is isolated means :: GLIB_000:def 52
a₂ .degree() = 0;
compatibility

proof end;

end;

:: deftheorem Def52 defines isolated GLIB_000:def 52 :

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
attr a₂ is endvertex means :Def53: :: GLIB_000:def 53
ex b₁ being set st
( a₂ .edgesInOut() = {b₁} & not b₁ Joins a₂,a₂,a₁ );

end;

:: deftheorem Def53 defines endvertex GLIB_000:def 53 :

definition

let c₁ be finite _Graph;
let c₂ be Vertex of c₁;
redefine attr a₂ is endvertex means :: GLIB_000:def 54
a₂ .degree() = 1;
compatibility

proof end;

end;

:: deftheorem Def54 defines endvertex GLIB_000:def 54 :

definition

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

end;

:: deftheorem Def55 defines Graph-yielding GLIB_000:def 55 :

:: deftheorem Def56 defines halting GLIB_000:def 56 :

definition

let c₁ be ManySortedSet of NAT ;
func c₁ .Lifespan() -> Nat means :: GLIB_000:def 57
( a₁ . a₂ = a₁ . (a₂ + 1) & ( for b₁ being Nat st a₁ . b₁ = a₁ . (b₁ + 1) holds
a₂ <= b₁ ) ) if a₁ is halting
otherwise a₂ = 0;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def57 defines .Lifespan() GLIB_000:def 57 :

definition

let c₁ be ManySortedSet of NAT ;
func c₁ .Result() -> set equals :: GLIB_000:def 58
a₁ . (a₁ .Lifespan() );
coherence ;

end;

:: deftheorem Def58 defines .Result() GLIB_000:def 58 :

registration

cluster Graph-yielding ManySortedSet of NAT ;
existence

proof end;

end;

definition

mode GraphSeq is Graph-yielding ManySortedSet of NAT ;

end;

definition

let c₁ be GraphSeq;
let c₂ be Nat;
func c₁ .-> c₂ -> _Graph equals :: GLIB_000:def 59
a₁ . a₂;
coherence by Def55;

end;

:: deftheorem Def59 defines .-> GLIB_000:def 59 :

definition

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

end;

:: deftheorem Def60 defines finite GLIB_000:def 60 :

:: deftheorem Def61 defines loopless GLIB_000:def 61 :

:: deftheorem Def62 defines trivial GLIB_000:def 62 :

:: deftheorem Def63 defines non-trivial GLIB_000:def 63 :

:: deftheorem Def64 defines non-multi GLIB_000:def 64 :

:: deftheorem Def65 defines non-Dmulti GLIB_000:def 65 :

:: deftheorem Def66 defines simple GLIB_000:def 66 :

:: deftheorem Def67 defines Dsimple GLIB_000:def 67 :

definition

let c₁ be GraphSeq;
redefine attr a₁ is halting means :: GLIB_000:def 68
ex b₁ being Nat st a₁ .-> b₁ = a₁ .-> (b₁ + 1);
compatibility

proof end;

end;

:: deftheorem Def68 defines halting GLIB_000:def 68 :

registration

cluster halting finite loopless trivial non-multi non-Dmulti simple Dsimple ManySortedSet of NAT ;
existence

proof end;

cluster halting finite loopless non-trivial non-multi non-Dmulti simple Dsimple ManySortedSet of NAT ;
existence

proof end;

end;

registration

let c₁ be finite GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> finite ;
coherence by Def60;

end;

registration

let c₁ be loopless GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> loopless ;
coherence by Def61;

end;

registration

let c₁ be trivial GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> trivial ;
coherence by Def62;

end;

registration

let c₁ be non-trivial GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> non trivial ;
coherence by Def63;

end;

registration

let c₁ be non-multi GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> non-multi non-Dmulti ;
coherence by Def64;

end;

registration

let c₁ be non-Dmulti GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> non-Dmulti ;
coherence by Def65;

end;

registration

let c₁ be simple GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> loopless non-multi non-Dmulti simple Dsimple ;
coherence by Def66;

end;

registration

let c₁ be Dsimple GraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> loopless non-Dmulti Dsimple ;
coherence by Def67;

end;

registration

cluster non-multi -> non-Dmulti ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster simple -> loopless non-multi non-Dmulti ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster loopless non-multi -> loopless non-multi non-Dmulti simple ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster loopless non-Dmulti -> Dsimple ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster Dsimple -> loopless non-Dmulti Dsimple ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster loopless trivial -> finite ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster trivial non-Dmulti -> finite ManySortedSet of NAT ;
coherence

proof end;

end;

theorem Th1: :: GLIB_000:1

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

theorem Th2: :: GLIB_000:2

for b₁ being set holds
( b₁ in _GraphSelectors iff ( b₁ = VertexSelector or b₁ = EdgeSelector or b₁ = SourceSelector or b₁ = TargetSelector ) ) by ENUMSET1:def 2;

theorem Th3: :: GLIB_000:3

for b₁ being _Graph holds _GraphSelectors c= dom b₁

proof end;

theorem Th4: :: GLIB_000:4

for b₁ being GraphStruct holds
( the_Vertices_of b₁ = b₁ . VertexSelector & the_Edges_of b₁ = b₁ . EdgeSelector & the_Source_of b₁ = b₁ . SourceSelector & the_Target_of b₁ = b₁ . TargetSelector ) ;

theorem Th5: :: GLIB_000:5

for b₁ being _Graph holds
( dom (the_Source_of b₁) = the_Edges_of b₁ & dom (the_Target_of b₁) = the_Edges_of b₁ & rng (the_Source_of b₁) c= the_Vertices_of b₁ & rng (the_Target_of b₁) c= the_Vertices_of b₁ ) by Lemma3;

theorem Th6: :: GLIB_000:6

canceled;

theorem Th7: :: GLIB_000:7

for b₁ being GraphStruct holds
( b₁ is [Graph-like] iff ( _GraphSelectors c= dom b₁ & not the_Vertices_of b₁ is empty & the_Source_of b₁ is Function of the_Edges_of b₁, the_Vertices_of b₁ & the_Target_of b₁ is Function of the_Edges_of b₁, the_Vertices_of b₁ ) ) by Lemma5;

theorem Th8: :: GLIB_000:8

for b₁ being non empty set
for b₂ being set
for b₃, b₄ being Function of b₂,b₁ holds
( the_Vertices_of (createGraph b₁,b₂,b₃,b₄) = b₁ & the_Edges_of (createGraph b₁,b₂,b₃,b₄) = b₂ & the_Source_of (createGraph b₁,b₂,b₃,b₄) = b₃ & the_Target_of (createGraph b₁,b₂,b₃,b₄) = b₄ ) by Lemma4;

theorem Th9: :: GLIB_000:9

for b₁ being GraphStruct
for b₂ being set
for b₃ being Nat holds dom (b₁ .set b₃,b₂) = (dom b₁) \/ {b₃}

proof end;

theorem Th10: :: GLIB_000:10

for b₁ being GraphStruct
for b₂ being set
for b₃ being Nat holds dom b₁ c= dom (b₁ .set b₃,b₂) by FUNCT_4:11;

theorem Th11: :: GLIB_000:11

for b₁ being GraphStruct
for b₂ being set
for b₃ being Nat holds (b₁ .set b₃,b₂) . b₃ = b₂

proof end;

theorem Th12: :: GLIB_000:12

for b₁ being GraphStruct
for b₂ being set
for b₃, b₄ being Nat st b₃ <> b₄ holds
b₁ . b₄ = (b₁ .set b₃,b₂) . b₄

proof end;

theorem Th13: :: GLIB_000:13

for b₁ being _Graph
for b₂ being set
for b₃ being Nat st not b₃ in _GraphSelectors holds
( the_Vertices_of b₁ = the_Vertices_of (b₁ .set b₃,b₂) & the_Edges_of b₁ = the_Edges_of (b₁ .set b₃,b₂) & the_Source_of b₁ = the_Source_of (b₁ .set b₃,b₂) & the_Target_of b₁ = the_Target_of (b₁ .set b₃,b₂) & b₁ .set b₃,b₂ is _Graph )

proof end;

theorem Th14: :: GLIB_000:14

for b₁ being GraphStruct
for b₂ being set holds
( the_Vertices_of (b₁ .set VertexSelector ,b₂) = b₂ & the_Edges_of (b₁ .set EdgeSelector ,b₂) = b₂ & the_Source_of (b₁ .set SourceSelector ,b₂) = b₂ & the_Target_of (b₁ .set TargetSelector ,b₂) = b₂ ) by Th11;

theorem Th15: :: GLIB_000:15

for b₁ being GraphStruct
for b₂, b₃ being set
for b₄, b₅ being Nat st b₄ <> b₅ holds
( b₄ in dom ((b₁ .set b₄,b₂) .set b₅,b₃) & b₅ in dom ((b₁ .set b₄,b₂) .set b₅,b₃) & ((b₁ .set b₄,b₂) .set b₅,b₃) . b₄ = b₂ & ((b₁ .set b₄,b₂) .set b₅,b₃) . b₅ = b₃ )

proof end;

theorem Th16: :: GLIB_000:16

for b₁ being _Graph
for b₂, b₃, b₄ being set st b₂ Joins b₃,b₄,b₁ holds
( b₃ in the_Vertices_of b₁ & b₄ in the_Vertices_of b₁ )

proof end;

theorem Th17: :: GLIB_000:17

for b₁ being _Graph
for b₂, b₃, b₄ being set st b₂ Joins b₃,b₄,b₁ holds
b₂ Joins b₄,b₃,b₁

proof end;

theorem Th18: :: GLIB_000:18

for b₁ being _Graph
for b₂, b₃, b₄, b₅, b₆ being set st b₂ Joins b₃,b₄,b₁ & b₂ Joins b₅,b₆,b₁ & not ( b₃ = b₅ & b₄ = b₆ ) holds
( b₃ = b₆ & b₄ = b₅ )

proof end;

theorem Th19: :: GLIB_000:19

for b₁ being _Graph
for b₂, b₃, b₄ being set holds
( b₂ Joins b₃,b₄,b₁ iff ( b₂ DJoins b₃,b₄,b₁ or b₂ DJoins b₄,b₃,b₁ ) ) by Lemma10;

theorem Th20: :: GLIB_000:20

for b₁ being _Graph
for b₂, b₃, b₄, b₅, b₆ being set st b₂ Joins b₃,b₄,b₁ & ( ( b₃ in b₅ & b₄ in b₆ ) or ( b₃ in b₆ & b₄ in b₅ ) ) holds
b₂ SJoins b₅,b₆,b₁

proof end;

theorem Th21: :: GLIB_000:21

for b₁ being _Graph holds
( b₁ is loopless iff for b₂, b₃ being set holds not b₃ Joins b₂,b₂,b₁ )

proof end;

theorem Th22: :: GLIB_000:22

for b₁ being finite loopless _Graph
for b₂ being Vertex of b₁ holds b₂ .degree() = card (b₂ .edgesInOut() )

proof end;

theorem Th23: :: GLIB_000:23

for b₁ being non trivial _Graph
for b₂ being Vertex of b₁ holds not (the_Vertices_of b₁) \ {b₂} is empty

proof end;

theorem Th24: :: GLIB_000:24

for b₁ being non trivial _Graph ex b₂, b₃ being Vertex of b₁ st b₂ <> b₃

proof end;

theorem Th25: :: GLIB_000:25

for b₁ being trivial _Graph ex b₂ being Vertex of b₁ st the_Vertices_of b₁ = {b₂}

proof end;

theorem Th26: :: GLIB_000:26

for b₁ being loopless trivial _Graph holds the_Edges_of b₁ = {}

proof end;

theorem Th27: :: GLIB_000:27

for b₁ being _Graph st the_Edges_of b₁ = {} holds
b₁ is simple

proof end;

theorem Th28: :: GLIB_000:28

for b₁ being finite _Graph holds b₁ .order() >= 1

proof end;

theorem Th29: :: GLIB_000:29

for b₁ being finite _Graph holds
( b₁ .order() = 1 iff b₁ is trivial ) by Def21, CARD_2:20;

theorem Th30: :: GLIB_000:30

for b₁ being finite _Graph holds
( b₁ .order() = 1 iff ex b₂ being Vertex of b₁ st the_Vertices_of b₁ = {b₂} )

proof end;

theorem Th31: :: GLIB_000:31

for b₁ being _Graph
for b₂, b₃ being set holds
( ( b₂ in the_Edges_of b₁ & ( (the_Source_of b₁) . b₂ in b₃ or (the_Target_of b₁) . b₂ in b₃ ) ) iff b₂ in b₁ .edgesInOut b₃ )

proof end;

theorem Th32: :: GLIB_000:32

for b₁ being _Graph
for b₂ being set holds
( b₁ .edgesInto b₂ c= b₁ .edgesInOut b₂ & b₁ .edgesOutOf b₂ c= b₁ .edgesInOut b₂ )

proof end;

theorem Th33: :: GLIB_000:33

for b₁ being _Graph holds the_Edges_of b₁ = b₁ .edgesInOut (the_Vertices_of b₁)

proof end;

theorem Th34: :: GLIB_000:34

for b₁ being _Graph
for b₂, b₃ being set holds
( ( b₂ in the_Edges_of b₁ & (the_Source_of b₁) . b₂ in b₃ & (the_Target_of b₁) . b₂ in b₃ ) iff b₂ in b₁ .edgesBetween b₃ ) by Lemma31;

theorem Th35: :: GLIB_000:35

for b₁ being _Graph
for b₂, b₃, b₄, b₅ being set st b₂ in b₃ & b₄ in b₃ & b₅ Joins b₂,b₄,b₁ holds
b₅ in b₁ .edgesBetween b₃

proof end;

theorem Th36: :: GLIB_000:36

for b₁ being _Graph
for b₂ being set holds b₁ .edgesBetween b₂ c= b₁ .edgesInOut b₂

proof end;

theorem Th37: :: GLIB_000:37

for b₁ being _Graph holds the_Edges_of b₁ = b₁ .edgesBetween (the_Vertices_of b₁)

proof end;

theorem Th38: :: GLIB_000:38

for b₁ being _Graph
for b₂ being set holds (the_Edges_of b₁) \ (b₁ .edgesInOut b₂) = b₁ .edgesBetween ((the_Vertices_of b₁) \ b₂)

proof end;

theorem Th39: :: GLIB_000:39

for b₁ being _Graph
for b₂, b₃ being set st b₂ c= b₃ holds
b₁ .edgesBetween b₂ c= b₁ .edgesBetween b₃

proof end;

theorem Th40: :: GLIB_000:40

for b₁ being _Graph
for b₂, b₃, b₄, b₅ being set st b₂ c= b₃ & b₄ c= b₅ holds
b₁ .edgesBetween b₂,b₄ c= b₁ .edgesBetween b₃,b₅

proof end;

theorem Th41: :: GLIB_000:41

for b₁ being _Graph
for b₂, b₃, b₄, b₅ being set st b₂ c= b₃ & b₄ c= b₅ holds
b₁ .edgesDBetween b₂,b₄ c= b₁ .edgesDBetween b₃,b₅

proof end;

theorem Th42: :: GLIB_000:42

for b₁ being _Graph
for b₂ being Vertex of b₁ holds
( b₂ .edgesIn() = b₁ .edgesDBetween (the_Vertices_of b₁),{b₂} & b₂ .edgesOut() = b₁ .edgesDBetween {b₂},(the_Vertices_of b₁) )

proof end;

theorem Th43: :: GLIB_000:43

for b₁ being _Graph holds b₁ is Subgraph of b₁ by Lemma24;

theorem Th44: :: GLIB_000:44

for b₁, b₂ being _Graph holds
( b₁ is Subgraph of b₂ & b₂ is Subgraph of b₁ iff ( the_Vertices_of b₁ = the_Vertices_of b₂ & the_Edges_of b₁ = the_Edges_of b₂ & the_Source_of b₁ = the_Source_of b₂ & the_Target_of b₁ = the_Target_of b₂ ) )

proof end;

theorem Th45: :: GLIB_000:45

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being set holds
( ( b₃ in the_Vertices_of b₂ implies b₃ in the_Vertices_of b₁ ) & ( b₃ in the_Edges_of b₂ implies b₃ in the_Edges_of b₁ ) ) ;

theorem Th46: :: GLIB_000:46

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Subgraph of b₂ holds b₃ is Subgraph of b₁

proof end;

theorem Th47: :: GLIB_000:47

for b₁ being _Graph
for b₂, b₃ being Subgraph of b₁ st the_Vertices_of b₂ c= the_Vertices_of b₃ & the_Edges_of b₂ c= the_Edges_of b₃ holds
b₂ is Subgraph of b₃

proof end;

theorem Th48: :: GLIB_000:48

for b₁ being _Graph
for b₂ being Subgraph of b₁ holds
( the_Source_of b₂ = (the_Source_of b₁) | (the_Edges_of b₂) & the_Target_of b₂ = (the_Target_of b₁) | (the_Edges_of b₂) )

proof end;

theorem Th49: :: GLIB_000:49

for b₁ being _Graph
for b₂, b₃, b₄, b₅ being set
for b₆ being inducedSubgraph of b₁,b₂,b₄
for b₇ being inducedSubgraph of b₁,b₃,b₅ st b₃ c= b₂ & b₅ c= b₄ & b₃ is non empty Subset of (the_Vertices_of b₁) & b₅ c= b₁ .edgesBetween b₃ holds
b₇ is Subgraph of b₆

proof end;

theorem Th50: :: GLIB_000:50

for b₁ being non trivial _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ holds
( the_Vertices_of b₃ = (the_Vertices_of b₁) \ {b₂} & the_Edges_of b₃ = b₁ .edgesBetween ((the_Vertices_of b₁) \ {b₂}) )

proof end;

theorem Th51: :: GLIB_000:51

for b₁ being finite non trivial _Graph
for b₂ being Vertex of b₁
for b₃ being removeVertex of b₁,b₂ holds
( (b₃ .order() ) + 1 = b₁ .order() & (b₃ .size() ) + (card (b₂ .edgesInOut() )) = b₁ .size() )

proof end;

theorem Th52: :: GLIB_000:52

for b₁ being _Graph
for b₂ being set
for b₃ being removeVertices of b₁,b₂ st b₂ c< the_Vertices_of b₁ holds
( the_Vertices_of b₃ = (the_Vertices_of b₁) \ b₂ & the_Edges_of b₃ = b₁ .edgesBetween ((the_Vertices_of b₁) \ b₂) )

proof end;

theorem Th53: :: GLIB_000:53

for b₁ being finite _Graph
for b₂ being Subset of (the_Vertices_of b₁)
for b₃ being removeVertices of b₁,b₂ st b₂ <> the_Vertices_of b₁ holds
( (b₃ .order() ) + (card b₂) = b₁ .order() & (b₃ .size() ) + (card (b₁ .edgesInOut b₂)) = b₁ .size() )

proof end;

theorem Th54: :: GLIB_000:54

for b₁ being _Graph
for b₂ being set
for b₃ being removeEdge of b₁,b₂ holds
( the_Vertices_of b₃ = the_Vertices_of b₁ & the_Edges_of b₃ = (the_Edges_of b₁) \ {b₂} )

proof end;

theorem Th55: :: GLIB_000:55

for b₁ being finite _Graph
for b₂ being set
for b₃ being removeEdge of b₁,b₂ holds
( b₁ .order() = b₃ .order() & ( b₂ in the_Edges_of b₁ implies (b₃ .size() ) + 1 = b₁ .size() ) )

proof end;

theorem Th56: :: GLIB_000:56

for b₁ being _Graph
for b₂ being set
for b₃ being removeEdges of b₁,b₂ holds
( the_Vertices_of b₃ = the_Vertices_of b₁ & the_Edges_of b₃ = (the_Edges_of b₁) \ b₂ )

proof end;

theorem Th57: :: GLIB_000:57

for b₁ being finite _Graph
for b₂ being set
for b₃ being removeEdges of b₁,b₂ holds b₁ .order() = b₃ .order() by Th56;

theorem Th58: :: GLIB_000:58

for b₁ being finite _Graph
for b₂ being Subset of (the_Edges_of b₁)
for b₃ being removeEdges of b₁,b₂ holds (b₃ .size() ) + (card b₂) = b₁ .size()

proof end;

theorem Th59: :: GLIB_000:59

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesIn() iff ( b₂ in the_Edges_of b₁ & (the_Target_of b₁) . b₂ = b₃ ) ) by Lemma33;

theorem Th60: :: GLIB_000:60

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesIn() iff ex b₄ being set st b₂ DJoins b₄,b₃,b₁ )

proof end;

theorem Th61: :: GLIB_000:61

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesOut() iff ( b₂ in the_Edges_of b₁ & (the_Source_of b₁) . b₂ = b₃ ) ) by Lemma34;

theorem Th62: :: GLIB_000:62

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesOut() iff ex b₄ being set st b₂ DJoins b₃,b₄,b₁ )

proof end;

theorem Th63: :: GLIB_000:63

for b₁ being _Graph
for b₂ being Vertex of b₁ holds b₂ .edgesInOut() = (b₂ .edgesIn() ) \/ (b₂ .edgesOut() ) ;

theorem Th64: :: GLIB_000:64

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesInOut() iff ( b₂ in the_Edges_of b₁ & ( (the_Source_of b₁) . b₂ = b₃ or (the_Target_of b₁) . b₂ = b₃ ) ) )

proof end;

theorem Th65: :: GLIB_000:65

for b₁ being _Graph
for b₂, b₃ being set
for b₄ being Vertex of b₁ st b₂ Joins b₄,b₃,b₁ holds
b₂ in b₄ .edgesInOut()

proof end;

theorem Th66: :: GLIB_000:66

for b₁ being _Graph
for b₂ being set
for b₃, b₄ being Vertex of b₁ holds
( not b₂ Joins b₃,b₄,b₁ or ( b₂ in b₃ .edgesIn() & b₂ in b₄ .edgesOut() ) or ( b₂ in b₄ .edgesIn() & b₂ in b₃ .edgesOut() ) )

proof end;

theorem Th67: :: GLIB_000:67

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesInOut() iff ex b₄ being Vertex of b₁ st b₂ Joins b₃,b₄,b₁ )

proof end;

theorem Th68: :: GLIB_000:68

for b₁ being _Graph
for b₂, b₃, b₄ being set
for b₅ being Vertex of b₁ st b₂ in b₅ .edgesInOut() & b₂ Joins b₃,b₄,b₁ & not b₅ = b₃ holds
b₅ = b₄

proof end;

theorem Th69: :: GLIB_000:69

for b₁ being _Graph
for b₂ being set
for b₃, b₄ being Vertex of b₁ st b₂ Joins b₃,b₄,b₁ holds
( b₃ .adj b₂ = b₄ & b₄ .adj b₂ = b₃ )

proof end;

theorem Th70: :: GLIB_000:70

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .edgesInOut() iff b₂ Joins b₃,b₃ .adj b₂,b₁ )

proof end;

theorem Th71: :: GLIB_000:71

for b₁ being finite _Graph
for b₂ being set
for b₃, b₄ being Vertex of b₁ st b₂ Joins b₃,b₄,b₁ holds
( 1 <= b₃ .degree() & 1 <= b₄ .degree() )

proof end;

theorem Th72: :: GLIB_000:72

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .inNeighbors() iff ex b₄ being set st b₄ DJoins b₂,b₃,b₁ )

proof end;

theorem Th73: :: GLIB_000:73

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .outNeighbors() iff ex b₄ being set st b₄ DJoins b₃,b₂,b₁ )

proof end;

theorem Th74: :: GLIB_000:74

for b₁ being _Graph
for b₂ being set
for b₃ being Vertex of b₁ holds
( b₂ in b₃ .allNeighbors() iff ex b₄ being set st b₄ Joins b₃,b₂,b₁ )

proof end;

theorem Th75: :: GLIB_000:75

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃, b₄, b₅ being set holds
( ( b₅ Joins b₃,b₄,b₂ implies b₅ Joins b₃,b₄,b₁ ) & ( b₅ DJoins b₃,b₄,b₂ implies b₅ DJoins b₃,b₄,b₁ ) & ( b₅ SJoins b₃,b₄,b₂ implies b₅ SJoins b₃,b₄,b₁ ) & ( b₅ DSJoins b₃,b₄,b₂ implies b₅ DSJoins b₃,b₄,b₁ ) )

proof end;

theorem Th76: :: GLIB_000:76

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃, b₄, b₅ being set st b₅ in the_Edges_of b₂ holds
( ( b₅ Joins b₃,b₄,b₁ implies b₅ Joins b₃,b₄,b₂ ) & ( b₅ DJoins b₃,b₄,b₁ implies b₅ DJoins b₃,b₄,b₂ ) & ( b₅ SJoins b₃,b₄,b₁ implies b₅ SJoins b₃,b₄,b₂ ) & ( b₅ DSJoins b₃,b₄,b₁ implies b₅ DSJoins b₃,b₄,b₂ ) )

proof end;

theorem Th77: :: GLIB_000:77

for b₁ being _Graph
for b₂ being spanning Subgraph of b₁
for b₃ being spanning Subgraph of b₂ holds b₃ is spanning Subgraph of b₁

proof end;

theorem Th78: :: GLIB_000:78

for b₁ being finite _Graph
for b₂ being Subgraph of b₁ holds
( b₂ .order() <= b₁ .order() & b₂ .size() <= b₁ .size() )

proof end;

theorem Th79: :: GLIB_000:79

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being set holds
( b₂ .edgesInto b₃ c= b₁ .edgesInto b₃ & b₂ .edgesOutOf b₃ c= b₁ .edgesOutOf b₃ & b₂ .edgesInOut b₃ c= b₁ .edgesInOut b₃ & b₂ .edgesBetween b₃ c= b₁ .edgesBetween b₃ )

proof end;

theorem Th80: :: GLIB_000:80

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃, b₄ being set holds
( b₂ .edgesBetween b₃,b₄ c= b₁ .edgesBetween b₃,b₄ & b₂ .edgesDBetween b₃,b₄ c= b₁ .edgesDBetween b₃,b₄ )

proof end;

theorem Th81: :: GLIB_000:81

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ holds
( b₄ .edgesIn() c= b₃ .edgesIn() & b₄ .edgesOut() c= b₃ .edgesOut() & b₄ .edgesInOut() c= b₃ .edgesInOut() )

proof end;

theorem Th82: :: GLIB_000:82

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ holds
( b₄ .edgesIn() = (b₃ .edgesIn() ) /\ (the_Edges_of b₂) & b₄ .edgesOut() = (b₃ .edgesOut() ) /\ (the_Edges_of b₂) & b₄ .edgesInOut() = (b₃ .edgesInOut() ) /\ (the_Edges_of b₂) )

proof end;

theorem Th83: :: GLIB_000:83

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂
for b₅ being set st b₃ = b₄ & b₅ in the_Edges_of b₂ holds
b₃ .adj b₅ = b₄ .adj b₅

proof end;

theorem Th84: :: GLIB_000:84

for b₁ being finite _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ holds
( b₄ .inDegree() <= b₃ .inDegree() & b₄ .outDegree() <= b₃ .outDegree() & b₄ .degree() <= b₃ .degree() )

proof end;

theorem Th85: :: GLIB_000:85

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ holds
( b₄ .inNeighbors() c= b₃ .inNeighbors() & b₄ .outNeighbors() c= b₃ .outNeighbors() & b₄ .allNeighbors() c= b₃ .allNeighbors() )

proof end;

theorem Th86: :: GLIB_000:86

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ & b₃ is isolated holds
b₄ is isolated

proof end;

theorem Th87: :: GLIB_000:87

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ & b₃ is endvertex & not b₄ is endvertex holds
b₄ is isolated

proof end;

theorem Th88: :: GLIB_000:88

for b₁, b₂, b₃ being _Graph st b₁ == b₂ & b₂ == b₃ holds
b₁ == b₃

proof end;

theorem Th89: :: GLIB_000:89

for b₁ being _Graph
for b₂, b₃ being Subgraph of b₁ st the_Vertices_of b₂ = the_Vertices_of b₃ & the_Edges_of b₂ = the_Edges_of b₃ holds
b₂ == b₃

proof end;

theorem Th90: :: GLIB_000:90

for b₁, b₂ being _Graph holds
( b₁ == b₂ iff ( b₁ is Subgraph of b₂ & b₂ is Subgraph of b₁ ) )

proof end;

theorem Th91: :: GLIB_000:91

for b₁, b₂ being _Graph
for b₃, b₄, b₅, b₆, b₇ being set st b₁ == b₂ holds
( ( b₃ Joins b₄,b₅,b₁ implies b₃ Joins b₄,b₅,b₂ ) & ( b₃ DJoins b₄,b₅,b₁ implies b₃ DJoins b₄,b₅,b₂ ) & ( b₃ SJoins b₆,b₇,b₁ implies b₃ SJoins b₆,b₇,b₂ ) & ( b₃ DSJoins b₆,b₇,b₁ implies b₃ DSJoins b₆,b₇,b₂ ) )

proof end;

theorem Th92: :: GLIB_000:92

for b₁, b₂ being _Graph st b₁ == b₂ holds
( ( b₁ is finite implies b₂ is finite ) & ( b₁ is loopless implies b₂ is loopless ) & ( b₁ is trivial implies b₂ is trivial ) & ( b₁ is non-multi implies b₂ is non-multi ) & ( b₁ is non-Dmulti implies b₂ is non-Dmulti ) & ( b₁ is simple implies b₂ is simple ) & ( b₁ is Dsimple implies b₂ is Dsimple ) )

proof end;

theorem Th93: :: GLIB_000:93

for b₁, b₂ being _Graph
for b₃, b₄ being set st b₁ == b₂ holds
( b₁ .order() = b₂ .order() & b₁ .size() = b₂ .size() & b₁ .edgesInto b₃ = b₂ .edgesInto b₃ & b₁ .edgesOutOf b₃ = b₂ .edgesOutOf b₃ & b₁ .edgesInOut b₃ = b₂ .edgesInOut b₃ & b₁ .edgesBetween b₃ = b₂ .edgesBetween b₃ & b₁ .edgesDBetween b₃,b₄ = b₂ .edgesDBetween b₃,b₄ )

proof end;

theorem Th94: :: GLIB_000:94

for b₁, b₂, b₃ being _Graph st b₁ == b₂ & b₃ is Subgraph of b₁ holds
b₃ is Subgraph of b₂

proof end;

theorem Th95: :: GLIB_000:95

for b₁, b₂, b₃ being _Graph st b₁ == b₂ & b₁ is Subgraph of b₃ holds
b₂ is Subgraph of b₃

proof end;

theorem Th96: :: GLIB_000:96

for b₁ being _Graph
for b₂, b₃ being set
for b₄, b₅ being inducedSubgraph of b₁,b₂,b₃ holds b₄ == b₅

proof end;

theorem Th97: :: GLIB_000:97

for b₁ being _Graph
for b₂ being inducedSubgraph of b₁,(the_Vertices_of b₁) holds b₁ == b₂

proof end;

theorem Th98: :: GLIB_000:98

for b₁, b₂ being _Graph
for b₃, b₄ being set
for b₅ being inducedSubgraph of b₁,b₃,b₄ st b₁ == b₂ holds
b₅ is inducedSubgraph of b₂,b₃,b₄

proof end;

theorem Th99: :: GLIB_000:99

for b₁, b₂ being _Graph
for b₃ being set
for b₄ being Vertex of b₁
for b₅ being Vertex of b₂ st b₄ = b₅ & b₁ == b₂ holds
( b₄ .edgesIn() = b₅ .edgesIn() & b₄ .edgesOut() = b₅ .edgesOut() & b₄ .edgesInOut() = b₅ .edgesInOut() & b₄ .adj b₃ = b₅ .adj b₃ & b₄ .inDegree() = b₅ .inDegree() & b₄ .outDegree() = b₅ .outDegree() & b₄ .degree() = b₅ .degree() & b₄ .inNeighbors() = b₅ .inNeighbors() & b₄ .outNeighbors() = b₅ .outNeighbors() & b₄ .allNeighbors() = b₅ .allNeighbors() )

proof end;

theorem Th100: :: GLIB_000:100

for b₁, b₂ being _Graph
for b₃ being Vertex of b₁
for b₄ being Vertex of b₂ st b₃ = b₄ & b₁ == b₂ holds
( ( b₃ is isolated implies b₄ is isolated ) & ( b₃ is endvertex implies b₄ is endvertex ) )

proof end;

theorem Th101: :: GLIB_000:101

for b₁ being _Graph
for b₂, b₃ being Subgraph of b₁ holds
( not b₂ c< b₃ or the_Vertices_of b₂ c< the_Vertices_of b₃ or the_Edges_of b₂ c< the_Edges_of b₃ )

proof end;

theorem Th102: :: GLIB_000:102

for b₁ being _Graph
for b₂, b₃ being Subgraph of b₁ holds
( not b₂ c< b₃ or ex b₄ being set st
( b₄ in the_Vertices_of b₃ & not b₄ in the_Vertices_of b₂ ) or ex b₄ being set st
( b₄ in the_Edges_of b₃ & not b₄ in the_Edges_of b₂ ) )

proof end;