:: GLIB_003 semantic presentation

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃ be FinSubsequence of c₂;
redefine func Seq as Seq c₃ -> FinSequence of a₁;
correctness

proof end;

end;

registration

let c₁ be real-yielding Relation;
let c₂ be set ;
cluster a₁ | a₂ -> real-yielding ;
coherence ;

end;

theorem Th1: :: GLIB_003:1

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀ being set
for b₁₁ being FinSequence st b₁₁ = ((((((((<*b₁*> ^ <*b₂*>) ^ <*b₃*>) ^ <*b₄*>) ^ <*b₅*>) ^ <*b₆*>) ^ <*b₇*>) ^ <*b₈*>) ^ <*b₉*>) ^ <*b₁₀*> holds
( len b₁₁ = 10 & b₁₁ . 1 = b₁ & b₁₁ . 2 = b₂ & b₁₁ . 3 = b₃ & b₁₁ . 4 = b₄ & b₁₁ . 5 = b₅ & b₁₁ . 6 = b₆ & b₁₁ . 7 = b₇ & b₁₁ . 8 = b₈ & b₁₁ . 9 = b₉ & b₁₁ . 10 = b₁₀ )

proof end;

theorem Th2: :: GLIB_003:2

for b₁ being FinSequence of REAL
for b₂ being FinSubsequence of b₁ st ( for b₃ being Nat st b₃ in dom b₁ holds
0 <= b₁ . b₃ ) holds
Sum (Seq b₂) <= Sum b₁

proof end;

definition

func WeightSelector -> Nat equals :: GLIB_003:def 1
5;
coherence ;
func ELabelSelector -> Nat equals :: GLIB_003:def 2
6;
coherence ;
func VLabelSelector -> Nat equals :: GLIB_003:def 3
7;
coherence ;

end;

:: deftheorem Def1 defines WeightSelector GLIB_003:def 1 :

:: deftheorem Def2 defines ELabelSelector GLIB_003:def 2 :

:: deftheorem Def3 defines VLabelSelector GLIB_003:def 3 :

definition

let c₁ be GraphStruct ;
attr a₁ is [Weighted] means :Def4: :: GLIB_003:def 4
( WeightSelector in dom a₁ & a₁ . WeightSelector is ManySortedSet of the_Edges_of a₁ );
attr a₁ is [ELabeled] means :Def5: :: GLIB_003:def 5
( ELabelSelector in dom a₁ & ex b₁ being Function st
( a₁ . ELabelSelector = b₁ & dom b₁ c= the_Edges_of a₁ ) );
attr a₁ is [VLabeled] means :Def6: :: GLIB_003:def 6
( VLabelSelector in dom a₁ & ex b₁ being Function st
( a₁ . VLabelSelector = b₁ & dom b₁ c= the_Vertices_of a₁ ) );

end;

:: deftheorem Def4 defines [Weighted] GLIB_003:def 4 :

:: deftheorem Def5 defines [ELabeled] GLIB_003:def 5 :

:: deftheorem Def6 defines [VLabeled] GLIB_003:def 6 :

registration

cluster [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct ;
existence

proof end;

end;

definition end;

definition

let c₁ be WGraph;
func the_Weight_of c₁ -> ManySortedSet of the_Edges_of a₁ equals :: GLIB_003:def 7
a₁ . WeightSelector ;
coherence by Def4;

end;

:: deftheorem Def7 defines the_Weight_of GLIB_003:def 7 :

definition

let c₁ be EGraph;
func the_ELabel_of c₁ -> Function equals :: GLIB_003:def 8
a₁ . ELabelSelector ;
coherence

proof end;

end;

:: deftheorem Def8 defines the_ELabel_of GLIB_003:def 8 :

definition

let c₁ be VGraph;
func the_VLabel_of c₁ -> Function equals :: GLIB_003:def 9
a₁ . VLabelSelector ;
coherence

proof end;

end;

:: deftheorem Def9 defines the_VLabel_of GLIB_003:def 9 :

Lemma5: for b₁ being EGraph holds dom (the_ELabel_of b₁) c= the_Edges_of b₁

proof end;

Lemma6: for b₁ being VGraph holds dom (the_VLabel_of b₁) c= the_Vertices_of b₁

proof end;

registration

let c₁ be _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] ;
coherence

proof end;

end;

Lemma7: for b₁ being _Graph
for b₂ being set holds
( b₁ .set WeightSelector ,b₂ == b₁ & b₁ .set ELabelSelector ,b₂ == b₁ & b₁ .set VLabelSelector ,b₂ == b₁ )

proof end;

registration

let c₁ be finite _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] finite ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] finite ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] finite ;
coherence

proof end;

end;

registration

let c₁ be loopless _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] loopless ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] loopless ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] loopless ;
coherence

proof end;

end;

registration

let c₁ be trivial _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] trivial ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] trivial ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] trivial ;
coherence

proof end;

end;

registration

let c₁ be non trivial _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] non trivial ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] non trivial ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] non trivial ;
coherence

proof end;

end;

registration

let c₁ be non-multi _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] non-multi ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] non-multi ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] non-multi ;
coherence

proof end;

end;

registration

let c₁ be non-Dmulti _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] non-Dmulti ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] non-Dmulti ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] non-Dmulti ;
coherence

proof end;

end;

registration

let c₁ be connected _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] connected ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] connected ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] connected ;
coherence

proof end;

end;

registration

let c₁ be acyclic _Graph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] loopless non-multi acyclic ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] loopless non-multi acyclic ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] loopless non-multi acyclic ;
coherence

proof end;

end;

registration

let c₁ be WGraph;
let c₂ be set ;
cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [Weighted] ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [Weighted] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be ManySortedSet of the_Edges_of c₁;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] [Weighted] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be non empty set ;
let c₃ be Function of the_Edges_of c₁,c₂;
cluster a₁ .set WeightSelector ,a₃ -> [Graph-like] [Weighted] ;
coherence

proof end;

end;

registration

let c₁ be EGraph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] [ELabeled] ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [ELabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be set ;
let c₃ be PartFunc of the_Edges_of c₁,c₂;
cluster a₁ .set ELabelSelector ,a₃ -> [Graph-like] [ELabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be ManySortedSet of the_Edges_of c₁;
cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [ELabeled] ;
coherence

proof end;

end;

registration

let c₁ be VGraph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] [VLabeled] ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [VLabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be set ;
let c₃ be PartFunc of the_Vertices_of c₁,c₂;
cluster a₁ .set VLabelSelector ,a₃ -> [Graph-like] [VLabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be ManySortedSet of the_Vertices_of c₁;
cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [VLabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
cluster a₁ .set ELabelSelector ,{} -> [Graph-like] [ELabeled] ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,{} -> [Graph-like] [VLabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
cluster [Weighted] [ELabeled] [VLabeled] Subgraph of a₁;
existence

proof end;

end;

definition

let c₁ be WGraph;
let c₂ be [Weighted] Subgraph of c₁;
attr a₂ is weight-inheriting means :Def10: :: GLIB_003:def 10
the_Weight_of a₂ = (the_Weight_of a₁) | (the_Edges_of a₂);

end;

:: deftheorem Def10 defines weight-inheriting GLIB_003:def 10 :

definition

let c₁ be EGraph;
let c₂ be [ELabeled] Subgraph of c₁;
attr a₂ is elabel-inheriting means :Def11: :: GLIB_003:def 11
the_ELabel_of a₂ = (the_ELabel_of a₁) | (the_Edges_of a₂);

end;

:: deftheorem Def11 defines elabel-inheriting GLIB_003:def 11 :

definition

let c₁ be VGraph;
let c₂ be [VLabeled] Subgraph of c₁;
attr a₂ is vlabel-inheriting means :Def12: :: GLIB_003:def 12
the_VLabel_of a₂ = (the_VLabel_of a₁) | (the_Vertices_of a₂);

end;

:: deftheorem Def12 defines vlabel-inheriting GLIB_003:def 12 :

registration

let c₁ be WGraph;
cluster [Weighted] weight-inheriting Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be EGraph;
cluster [ELabeled] elabel-inheriting Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be VGraph;
cluster [VLabeled] vlabel-inheriting Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be WEGraph;
cluster [Weighted] [ELabeled] weight-inheriting elabel-inheriting Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be WVGraph;
cluster [Weighted] [VLabeled] weight-inheriting vlabel-inheriting Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be EVGraph;
cluster [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting Subgraph of a₁;
existence

proof end;

end;

registration

let c₁ be WEVGraph;
cluster [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting Subgraph of a₁;
existence

proof end;

end;

definition

let c₁ be WGraph;
mode WSubgraph of a₁ is [Weighted] weight-inheriting Subgraph of a₁;

end;

definition

let c₁ be EGraph;
mode ESubgraph of a₁ is [ELabeled] elabel-inheriting Subgraph of a₁;

end;

definition

let c₁ be VGraph;
mode VSubgraph of a₁ is [VLabeled] vlabel-inheriting Subgraph of a₁;

end;

definition

let c₁ be WEGraph;
mode WESubgraph of a₁ is [Weighted] [ELabeled] weight-inheriting elabel-inheriting Subgraph of a₁;

end;

definition

let c₁ be WVGraph;
mode WVSubgraph of a₁ is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting Subgraph of a₁;

end;

definition

let c₁ be EVGraph;
mode EVSubgraph of a₁ is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting Subgraph of a₁;

end;

definition

let c₁ be WEVGraph;
mode WEVSubgraph of a₁ is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting Subgraph of a₁;

end;

registration

let c₁ be _Graph;
let c₂, c₃ be set ;
cluster [Weighted] [ELabeled] [VLabeled] inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be WGraph;
let c₂, c₃ be set ;
cluster [Weighted] weight-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be EGraph;
let c₂, c₃ be set ;
cluster [ELabeled] elabel-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be VGraph;
let c₂, c₃ be set ;
cluster [VLabeled] vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be WEGraph;
let c₂, c₃ be set ;
cluster [Weighted] [ELabeled] weight-inheriting elabel-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be WVGraph;
let c₂, c₃ be set ;
cluster [Weighted] [VLabeled] weight-inheriting vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be EVGraph;
let c₂, c₃ be set ;
cluster [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

registration

let c₁ be WEVGraph;
let c₂, c₃ be set ;
cluster [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;
existence

proof end;

end;

definition

let c₁ be WGraph;
let c₂, c₃ be set ;
mode inducedWSubgraph of a₁,a₂,a₃ is [Weighted] weight-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be EGraph;
let c₂, c₃ be set ;
mode inducedESubgraph of a₁,a₂,a₃ is [ELabeled] elabel-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be VGraph;
let c₂, c₃ be set ;
mode inducedVSubgraph of a₁,a₂,a₃ is [VLabeled] vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be WEGraph;
let c₂, c₃ be set ;
mode inducedWESubgraph of a₁,a₂,a₃ is [Weighted] [ELabeled] weight-inheriting elabel-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be WVGraph;
let c₂, c₃ be set ;
mode inducedWVSubgraph of a₁,a₂,a₃ is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be EVGraph;
let c₂, c₃ be set ;
mode inducedEVSubgraph of a₁,a₂,a₃ is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be WEVGraph;
let c₂, c₃ be set ;
mode inducedWEVSubgraph of a₁,a₂,a₃ is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting inducedSubgraph of a₁,a₂,a₃;

end;

definition

let c₁ be WGraph;
let c₂ be set ;
mode inducedWSubgraph of a₁,a₂ is inducedWSubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be EGraph;
let c₂ be set ;
mode inducedESubgraph of a₁,a₂ is inducedESubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be VGraph;
let c₂ be set ;
mode inducedVSubgraph of a₁,a₂ is inducedVSubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be WEGraph;
let c₂ be set ;
mode inducedWESubgraph of a₁,a₂ is inducedWESubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be WVGraph;
let c₂ be set ;
mode inducedWVSubgraph of a₁,a₂ is inducedWVSubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be EVGraph;
let c₂ be set ;
mode inducedEVSubgraph of a₁,a₂ is inducedEVSubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be WEVGraph;
let c₂ be set ;
mode inducedWEVSubgraph of a₁,a₂ is inducedWEVSubgraph of a₁,a₂,a₁ .edgesBetween a₂;

end;

definition

let c₁ be WGraph;
attr a₁ is real-weighted means :Def13: :: GLIB_003:def 13
the_Weight_of a₁ is real-yielding;

end;

:: deftheorem Def13 defines real-weighted GLIB_003:def 13 :

definition

let c₁ be WGraph;
attr a₁ is nonnegative-weighted means :Def14: :: GLIB_003:def 14
rng (the_Weight_of a₁) c= Real>=0 ;

end;

:: deftheorem Def14 defines nonnegative-weighted GLIB_003:def 14 :

registration

cluster nonnegative-weighted -> real-weighted GraphStruct ;
coherence

proof end;

end;

definition

let c₁ be EGraph;
attr a₁ is real-elabeled means :Def15: :: GLIB_003:def 15
the_ELabel_of a₁ is real-yielding;

end;

:: deftheorem Def15 defines real-elabeled GLIB_003:def 15 :

definition

let c₁ be VGraph;
attr a₁ is real-vlabeled means :Def16: :: GLIB_003:def 16
the_VLabel_of a₁ is real-yielding;

end;

:: deftheorem Def16 defines real-vlabeled GLIB_003:def 16 :

definition

let c₁ be WEVGraph;
attr a₁ is real-WEV means :Def17: :: GLIB_003:def 17
( a₁ is real-weighted & a₁ is real-elabeled & a₁ is real-vlabeled );

end;

:: deftheorem Def17 defines real-WEV GLIB_003:def 17 :

registration

cluster real-WEV -> real-weighted real-elabeled real-vlabeled GraphStruct ;
coherence by Def17;
cluster real-weighted real-elabeled real-vlabeled -> real-WEV GraphStruct ;
coherence by Def17;

end;

registration

let c₁ be _Graph;
let c₂ be Function of the_Edges_of c₁, REAL ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] [Weighted] real-weighted ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be PartFunc of the_Edges_of c₁, REAL ;
cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [ELabeled] real-elabeled ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be real-yielding ManySortedSet of the_Edges_of c₁;
cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [ELabeled] real-elabeled ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be PartFunc of the_Vertices_of c₁, REAL ;
cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [VLabeled] real-vlabeled ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be real-yielding ManySortedSet of the_Vertices_of c₁;
cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [VLabeled] real-vlabeled ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
cluster a₁ .set ELabelSelector ,{} -> [Graph-like] [ELabeled] real-elabeled ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,{} -> [Graph-like] [VLabeled] real-vlabeled ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Vertex of c₁;
let c₃ be real number ;
cluster a₁ .set VLabelSelector ,(a₂ .--> a₃) -> [Graph-like] [VLabeled] ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Vertex of c₁;
let c₃ be real number ;
cluster a₁ .set VLabelSelector ,(a₂ .--> a₃) -> [Graph-like] [VLabeled] real-vlabeled ;
coherence

proof end;

end;

registration

cluster finite trivial Tree-like real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV GraphStruct ;
existence

proof end;

cluster finite non trivial Tree-like real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV GraphStruct ;
existence

proof end;

end;

registration

let c₁ be finite WGraph;
cluster the_Weight_of a₁ -> finite ;
coherence

proof end;

end;

registration

let c₁ be finite EGraph;
cluster the_ELabel_of a₁ -> finite ;
coherence

proof end;

end;

registration

let c₁ be finite VGraph;
cluster the_VLabel_of a₁ -> finite ;
coherence

proof end;

end;

registration

let c₁ be real-weighted WGraph;
cluster the_Weight_of a₁ -> real-yielding ;
coherence by Def13;

end;

registration

let c₁ be real-elabeled EGraph;
cluster the_ELabel_of a₁ -> real-yielding ;
coherence by Def15;

end;

registration

let c₁ be real-vlabeled VGraph;
cluster the_VLabel_of a₁ -> real-yielding ;
coherence by Def16;

end;

registration

let c₁ be real-weighted WGraph;
let c₂ be set ;
cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [Weighted] real-weighted ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [Weighted] real-weighted ;
coherence

proof end;

end;

registration

let c₁ be nonnegative-weighted WGraph;
let c₂ be set ;
cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [Weighted] real-weighted nonnegative-weighted ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [Weighted] real-weighted nonnegative-weighted ;
coherence

proof end;

end;

registration

let c₁ be real-elabeled EGraph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] [ELabeled] real-elabeled ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> [Graph-like] [ELabeled] real-elabeled ;
coherence

proof end;

end;

registration

let c₁ be real-vlabeled VGraph;
let c₂ be set ;
cluster a₁ .set WeightSelector ,a₂ -> [Graph-like] [VLabeled] real-vlabeled ;
coherence

proof end;

cluster a₁ .set ELabelSelector ,a₂ -> [Graph-like] [VLabeled] real-vlabeled ;
coherence

proof end;

end;

definition

let c₁ be WGraph;
let c₂ be Walk of c₁;
func c₂ .weightSeq() -> FinSequence means :Def18: :: GLIB_003:def 18
( len a₃ = len (a₂ .edgeSeq() ) & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₃ holds
a₃ . b₁ = (the_Weight_of a₁) . ((a₂ .edgeSeq() ) . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :

definition

let c₁ be real-weighted WGraph;
let c₂ be Walk of c₁;
redefine func .weightSeq() as c₂ .weightSeq() -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let c₁ be real-weighted WGraph;
let c₂ be Walk of c₁;
func c₂ .cost() -> Real equals :: GLIB_003:def 19
Sum (a₂ .weightSeq() );
coherence ;

end;

:: deftheorem Def19 defines .cost() GLIB_003:def 19 :

Lemma17: for b₁, b₂, b₃, b₄ being set
for b₅ being PartFunc of b₃,b₄ st b₁ in b₃ & b₂ in b₄ holds
b₅ +* (b₁ .--> b₂) is PartFunc of b₃,b₄

proof end;

definition

let c₁ be EGraph;
func c₁ .labeledE() -> Subset of (the_Edges_of a₁) equals :: GLIB_003:def 20
dom (the_ELabel_of a₁);
coherence by Lemma5;

end;

:: deftheorem Def20 defines .labeledE() GLIB_003:def 20 :

definition

let c₁ be EGraph;
let c₂, c₃ be set ;
func c₁ .labelEdge c₂,c₃ -> EGraph equals :Def21: :: GLIB_003:def 21
a₁ .set ELabelSelector ,((the_ELabel_of a₁) +* (a₂ .--> a₃)) if a₂ in the_Edges_of a₁
otherwise a₁;
coherence

proof end;

consistency ;

end;

:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :

registration

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

proof end;

end;

registration

let c₁ be loopless EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> loopless ;
coherence

proof end;

end;

registration

let c₁ be trivial EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> trivial ;
coherence

proof end;

end;

registration

let c₁ be non trivial EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> non trivial ;
coherence

proof end;

end;

registration

let c₁ be non-multi EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> non-multi ;
coherence

proof end;

end;

registration

let c₁ be non-Dmulti EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> non-Dmulti ;
coherence

proof end;

end;

registration

let c₁ be connected EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> connected ;
coherence

proof end;

end;

registration

let c₁ be acyclic EGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> loopless non-multi acyclic ;
coherence

proof end;

end;

registration

let c₁ be WEGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> [Weighted] ;
coherence

proof end;

end;

registration

let c₁ be EVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> [VLabeled] ;
coherence

proof end;

end;

registration

let c₁ be real-weighted WEGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> [Weighted] real-weighted ;
coherence

proof end;

end;

registration

let c₁ be nonnegative-weighted WEGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> [Weighted] real-weighted nonnegative-weighted ;
coherence

proof end;

end;

registration

let c₁ be real-elabeled EGraph;
let c₂ be set ;
let c₃ be Real;
cluster a₁ .labelEdge a₂,a₃ -> real-elabeled ;
coherence

proof end;

end;

registration

let c₁ be real-vlabeled EVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelEdge a₂,a₃ -> [VLabeled] real-vlabeled ;
coherence

proof end;

end;

definition

let c₁ be VGraph;
let c₂, c₃ be set ;
func c₁ .labelVertex c₂,c₃ -> VGraph equals :Def22: :: GLIB_003:def 22
a₁ .set VLabelSelector ,((the_VLabel_of a₁) +* (a₂ .--> a₃)) if a₂ in the_Vertices_of a₁
otherwise a₁;
coherence

proof end;

consistency ;

end;

:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :

definition

let c₁ be VGraph;
func c₁ .labeledV() -> Subset of (the_Vertices_of a₁) equals :: GLIB_003:def 23
dom (the_VLabel_of a₁);
coherence by Lemma6;

end;

:: deftheorem Def23 defines .labeledV() GLIB_003:def 23 :

registration

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

proof end;

end;

registration

let c₁ be loopless VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> loopless ;
coherence

proof end;

end;

registration

let c₁ be trivial VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> trivial ;
coherence

proof end;

end;

registration

let c₁ be non trivial VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> non trivial ;
coherence

proof end;

end;

registration

let c₁ be non-multi VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> non-multi ;
coherence

proof end;

end;

registration

let c₁ be non-Dmulti VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> non-Dmulti ;
coherence

proof end;

end;

registration

let c₁ be connected VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> connected ;
coherence

proof end;

end;

registration

let c₁ be acyclic VGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> loopless non-multi acyclic ;
coherence

proof end;

end;

registration

let c₁ be WVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> [Weighted] ;
coherence

proof end;

end;

registration

let c₁ be EVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> [ELabeled] ;
coherence

proof end;

end;

registration

let c₁ be real-weighted WVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> [Weighted] real-weighted ;
coherence

proof end;

end;

registration

let c₁ be nonnegative-weighted WVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> [Weighted] real-weighted nonnegative-weighted ;
coherence

proof end;

end;

registration

let c₁ be real-elabeled EVGraph;
let c₂, c₃ be set ;
cluster a₁ .labelVertex a₂,a₃ -> [ELabeled] real-elabeled ;
coherence

proof end;

end;

registration

let c₁ be real-vlabeled VGraph;
let c₂ be set ;
let c₃ be Real;
cluster a₁ .labelVertex a₂,a₃ -> real-vlabeled ;
coherence

proof end;

end;

registration

let c₁ be real-weighted WGraph;
cluster -> real-weighted Subgraph of a₁;
coherence

proof end;

end;

registration

let c₁ be nonnegative-weighted WGraph;
cluster -> real-weighted nonnegative-weighted Subgraph of a₁;
coherence

proof end;

end;

registration

let c₁ be real-elabeled EGraph;
cluster -> real-elabeled Subgraph of a₁;
coherence

proof end;

end;

registration

let c₁ be real-vlabeled VGraph;
cluster -> real-vlabeled Subgraph of a₁;
coherence

proof end;

end;

definition

let c₁ be GraphSeq;
attr a₁ is [Weighted] means :Def24: :: GLIB_003:def 24
for b₁ being Nat holds a₁ .-> b₁ is [Weighted];
attr a₁ is [ELabeled] means :Def25: :: GLIB_003:def 25
for b₁ being Nat holds a₁ .-> b₁ is [ELabeled];
attr a₁ is [VLabeled] means :Def26: :: GLIB_003:def 26
for b₁ being Nat holds a₁ .-> b₁ is [VLabeled];

end;

:: deftheorem Def24 defines [Weighted] GLIB_003:def 24 :

:: deftheorem Def25 defines [ELabeled] GLIB_003:def 25 :

:: deftheorem Def26 defines [VLabeled] GLIB_003:def 26 :

registration

cluster [Weighted] [ELabeled] [VLabeled] ManySortedSet of NAT ;
existence

proof end;

end;

definition end;

registration

let c₁ be WGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [Weighted] ;
coherence by Def24;

end;

registration

let c₁ be EGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [ELabeled] ;
coherence by Def25;

end;

registration

let c₁ be VGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [VLabeled] ;
coherence by Def26;

end;

definition

let c₁ be WGraphSeq;
attr a₁ is real-weighted means :Def27: :: GLIB_003:def 27
for b₁ being Nat holds a₁ .-> b₁ is real-weighted;
attr a₁ is nonnegative-weighted means :Def28: :: GLIB_003:def 28
for b₁ being Nat holds a₁ .-> b₁ is nonnegative-weighted;

end;

:: deftheorem Def27 defines real-weighted GLIB_003:def 27 :

:: deftheorem Def28 defines nonnegative-weighted GLIB_003:def 28 :

definition

let c₁ be EGraphSeq;
attr a₁ is real-elabeled means :Def29: :: GLIB_003:def 29
for b₁ being Nat holds a₁ .-> b₁ is real-elabeled;

end;

:: deftheorem Def29 defines real-elabeled GLIB_003:def 29 :

definition

let c₁ be VGraphSeq;
attr a₁ is real-vlabeled means :Def30: :: GLIB_003:def 30
for b₁ being Nat holds a₁ .-> b₁ is real-vlabeled;

end;

:: deftheorem Def30 defines real-vlabeled GLIB_003:def 30 :

definition

let c₁ be WEVGraphSeq;
attr a₁ is real-WEV means :Def31: :: GLIB_003:def 31
for b₁ being Nat holds a₁ .-> b₁ is real-WEV;

end;

:: deftheorem Def31 defines real-WEV GLIB_003:def 31 :

registration

cluster real-WEV -> real-weighted real-elabeled real-vlabeled ManySortedSet of NAT ;
coherence

proof end;

cluster real-weighted real-elabeled real-vlabeled -> real-WEV ManySortedSet of NAT ;
coherence

proof end;

end;

registration

cluster halting finite loopless trivial non-multi simple Tree-like real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV ManySortedSet of NAT ;
existence

proof end;

end;

registration

let c₁ be real-weighted WGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [Weighted] real-weighted ;
coherence by Def27;

end;

registration

let c₁ be nonnegative-weighted WGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [Weighted] real-weighted nonnegative-weighted ;
coherence by Def28;

end;

registration

let c₁ be real-elabeled EGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [ELabeled] real-elabeled ;
coherence by Def29;

end;

registration

let c₁ be real-vlabeled VGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> [VLabeled] real-vlabeled ;
coherence by Def30;

end;

theorem Th3: :: GLIB_003:3

( WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7 ) ;

theorem Th4: :: GLIB_003:4

( ( for b₁ being WGraph holds the_Weight_of b₁ = b₁ . WeightSelector ) & ( for b₁ being EGraph holds the_ELabel_of b₁ = b₁ . ELabelSelector ) & ( for b₁ being VGraph holds the_VLabel_of b₁ = b₁ . VLabelSelector ) ) ;

theorem Th5: :: GLIB_003:5

canceled;

theorem Th6: :: GLIB_003:6

for b₁ being EGraph holds dom (the_ELabel_of b₁) c= the_Edges_of b₁ by Lemma5;

theorem Th7: :: GLIB_003:7

for b₁ being VGraph holds dom (the_VLabel_of b₁) c= the_Vertices_of b₁ by Lemma6;

theorem Th8: :: GLIB_003:8

for b₁ being _Graph
for b₂ being set holds
( b₁ == b₁ .set WeightSelector ,b₂ & b₁ == b₁ .set ELabelSelector ,b₂ & b₁ == b₁ .set VLabelSelector ,b₂ ) by Lemma7;

theorem Th9: :: GLIB_003:9

for b₁ being EGraph
for b₂ being set holds the_ELabel_of b₁ = the_ELabel_of (b₁ .set WeightSelector ,b₂) by GLIB_000:12;

theorem Th10: :: GLIB_003:10

for b₁ being VGraph
for b₂ being set holds the_VLabel_of b₁ = the_VLabel_of (b₁ .set WeightSelector ,b₂) by GLIB_000:12;

theorem Th11: :: GLIB_003:11

for b₁ being WGraph
for b₂ being set holds the_Weight_of b₁ = the_Weight_of (b₁ .set ELabelSelector ,b₂) by GLIB_000:12;

theorem Th12: :: GLIB_003:12

for b₁ being VGraph
for b₂ being set holds the_VLabel_of b₁ = the_VLabel_of (b₁ .set ELabelSelector ,b₂) by GLIB_000:12;

theorem Th13: :: GLIB_003:13

for b₁ being WGraph
for b₂ being set holds the_Weight_of b₁ = the_Weight_of (b₁ .set VLabelSelector ,b₂) by GLIB_000:12;

theorem Th14: :: GLIB_003:14

for b₁ being EGraph
for b₂ being set holds the_ELabel_of b₁ = the_ELabel_of (b₁ .set VLabelSelector ,b₂) by GLIB_000:12;

theorem Th15: :: GLIB_003:15

for b₁, b₂, b₃ being WGraph st b₁ == b₂ & the_Weight_of b₁ = the_Weight_of b₂ & b₁ is WSubgraph of b₃ holds
b₂ is WSubgraph of b₃

proof end;

theorem Th16: :: GLIB_003:16

for b₁ being WGraph
for b₂ being WSubgraph of b₁
for b₃ being WSubgraph of b₂ holds b₃ is WSubgraph of b₁

proof end;

theorem Th17: :: GLIB_003:17

for b₁, b₂ being WGraph
for b₃ being WSubgraph of b₁ st b₁ == b₂ & the_Weight_of b₁ = the_Weight_of b₂ holds
b₃ is WSubgraph of b₂

proof end;

theorem Th18: :: GLIB_003:18

for b₁ being WGraph
for b₂ being WSubgraph of b₁
for b₃ being set st b₃ in the_Edges_of b₂ holds
(the_Weight_of b₂) . b₃ = (the_Weight_of b₁) . b₃

proof end;

theorem Th19: :: GLIB_003:19

for b₁ being WGraph
for b₂ being Walk of b₁ st b₂ is trivial holds
b₂ .weightSeq() = {}

proof end;

theorem Th20: :: GLIB_003:20

for b₁ being WGraph
for b₂ being Walk of b₁ holds len (b₂ .weightSeq() ) = b₂ .length()

proof end;

theorem Th21: :: GLIB_003:21

for b₁ being WGraph
for b₂, b₃, b₄ being set st b₄ Joins b₂,b₃,b₁ holds
(b₁ .walkOf b₂,b₄,b₃) .weightSeq() = <*((the_Weight_of b₁) . b₄)*>

proof end;

theorem Th22: :: GLIB_003:22

for b₁ being WGraph
for b₂ being Walk of b₁ holds (b₂ .reverse() ) .weightSeq() = Rev (b₂ .weightSeq() )

proof end;

theorem Th23: :: GLIB_003:23

for b₁ being WGraph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .weightSeq() = (b₂ .weightSeq() ) ^ (b₃ .weightSeq() )

proof end;

theorem Th24: :: GLIB_003:24

for b₁ being WGraph
for b₂ being Walk of b₁
for b₃ being set st b₃ in (b₂ .last() ) .edgesInOut() holds
(b₂ .addEdge b₃) .weightSeq() = (b₂ .weightSeq() ) ^ <*((the_Weight_of b₁) . b₃)*>

proof end;

theorem Th25: :: GLIB_003:25

for b₁ being real-weighted WGraph
for b₂ being Walk of b₁
for b₃ being Subwalk of b₂ ex b₄ being FinSubsequence of b₂ .weightSeq() st b₃ .weightSeq() = Seq b₄

proof end;

theorem Th26: :: GLIB_003:26

for b₁, b₂ being WGraph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ & the_Weight_of b₁ = the_Weight_of b₂ holds
b₃ .weightSeq() = b₄ .weightSeq()

proof end;

theorem Th27: :: GLIB_003:27

for b₁ being WGraph
for b₂ being WSubgraph of b₁
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .weightSeq() = b₄ .weightSeq()

proof end;

theorem Th28: :: GLIB_003:28

for b₁ being real-weighted WGraph
for b₂ being Walk of b₁ st b₂ is trivial holds
b₂ .cost() = 0 by RVSUM_1:102, Th19;

theorem Th29: :: GLIB_003:29

for b₁ being real-weighted WGraph
for b₂, b₃ being Vertex of b₁
for b₄ being set st b₄ Joins b₂,b₃,b₁ holds
(b₁ .walkOf b₂,b₄,b₃) .cost() = (the_Weight_of b₁) . b₄

proof end;

theorem Th30: :: GLIB_003:30

for b₁ being real-weighted WGraph
for b₂ being Walk of b₁ holds b₂ .cost() = (b₂ .reverse() ) .cost()

proof end;

theorem Th31: :: GLIB_003:31

for b₁ being real-weighted WGraph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .cost() = (b₂ .cost() ) + (b₃ .cost() )

proof end;

theorem Th32: :: GLIB_003:32

for b₁ being real-weighted WGraph
for b₂ being Walk of b₁
for b₃ being set st b₃ in (b₂ .last() ) .edgesInOut() holds
(b₂ .addEdge b₃) .cost() = (b₂ .cost() ) + ((the_Weight_of b₁) . b₃)

proof end;

theorem Th33: :: GLIB_003:33

for b₁, b₂ being real-weighted WGraph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ & the_Weight_of b₁ = the_Weight_of b₂ holds
b₃ .cost() = b₄ .cost() by Th26;

theorem Th34: :: GLIB_003:34

for b₁ being real-weighted WGraph
for b₂ being WSubgraph of b₁
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .cost() = b₄ .cost() by Th27;

theorem Th35: :: GLIB_003:35

for b₁ being nonnegative-weighted WGraph
for b₂ being Walk of b₁
for b₃ being Nat st b₃ in dom (b₂ .weightSeq() ) holds
0 <= (b₂ .weightSeq() ) . b₃

proof end;

theorem Th36: :: GLIB_003:36

for b₁ being nonnegative-weighted WGraph
for b₂ being Walk of b₁ holds 0 <= b₂ .cost()

proof end;

theorem Th37: :: GLIB_003:37

for b₁ being nonnegative-weighted WGraph
for b₂ being Walk of b₁
for b₃ being Subwalk of b₂ holds b₃ .cost() <= b₂ .cost()

proof end;

theorem Th38: :: GLIB_003:38

for b₁ being nonnegative-weighted WGraph
for b₂ being set st b₂ in the_Edges_of b₁ holds
0 <= (the_Weight_of b₁) . b₂

proof end;

theorem Th39: :: GLIB_003:39

for b₁ being EGraph
for b₂, b₃ being set st b₂ in the_Edges_of b₁ holds
the_ELabel_of (b₁ .labelEdge b₂,b₃) = (the_ELabel_of b₁) +* (b₂ .--> b₃)

proof end;

theorem Th40: :: GLIB_003:40

for b₁ being EGraph
for b₂, b₃ being set st b₂ in the_Edges_of b₁ holds
(the_ELabel_of (b₁ .labelEdge b₂,b₃)) . b₂ = b₃

proof end;

theorem Th41: :: GLIB_003:41

for b₁ being EGraph
for b₂, b₃ being set holds b₁ == b₁ .labelEdge b₂,b₃

proof end;

theorem Th42: :: GLIB_003:42

for b₁ being WEGraph
for b₂, b₃ being set holds the_Weight_of b₁ = the_Weight_of (b₁ .labelEdge b₂,b₃)

proof end;

theorem Th43: :: GLIB_003:43

for b₁ being EVGraph
for b₂, b₃ being set holds the_VLabel_of b₁ = the_VLabel_of (b₁ .labelEdge b₂,b₃)

proof end;

theorem Th44: :: GLIB_003:44

for b₁ being EGraph
for b₂, b₃, b₄ being set st b₂ <> b₃ holds
(the_ELabel_of (b₁ .labelEdge b₂,b₄)) . b₃ = (the_ELabel_of b₁) . b₃

proof end;

theorem Th45: :: GLIB_003:45

for b₁ being VGraph
for b₂, b₃ being set st b₂ in the_Vertices_of b₁ holds
the_VLabel_of (b₁ .labelVertex b₂,b₃) = (the_VLabel_of b₁) +* (b₂ .--> b₃)

proof end;

theorem Th46: :: GLIB_003:46

for b₁ being VGraph
for b₂, b₃ being set st b₂ in the_Vertices_of b₁ holds
(the_VLabel_of (b₁ .labelVertex b₂,b₃)) . b₂ = b₃

proof end;

theorem Th47: :: GLIB_003:47

for b₁ being VGraph
for b₂, b₃ being set holds b₁ == b₁ .labelVertex b₂,b₃

proof end;

theorem Th48: :: GLIB_003:48

for b₁ being WVGraph
for b₂, b₃ being set holds the_Weight_of b₁ = the_Weight_of (b₁ .labelVertex b₂,b₃)

proof end;

theorem Th49: :: GLIB_003:49

for b₁ being EVGraph
for b₂, b₃ being set holds the_ELabel_of b₁ = the_ELabel_of (b₁ .labelVertex b₂,b₃)

proof end;

theorem Th50: :: GLIB_003:50

for b₁ being VGraph
for b₂, b₃, b₄ being set st b₂ <> b₃ holds
(the_VLabel_of (b₁ .labelVertex b₂,b₄)) . b₃ = (the_VLabel_of b₁) . b₃

proof end;

theorem Th51: :: GLIB_003:51

for b₁, b₂ being EGraph st the_ELabel_of b₁ = the_ELabel_of b₂ holds
b₁ .labeledE() = b₂ .labeledE() ;

theorem Th52: :: GLIB_003:52

for b₁ being EGraph
for b₂, b₃ being set st b₂ in the_Edges_of b₁ holds
(b₁ .labelEdge b₂,b₃) .labeledE() = (b₁ .labeledE() ) \/ {b₂}

proof end;

theorem Th53: :: GLIB_003:53

for b₁ being EGraph
for b₂, b₃ being set st b₂ in the_Edges_of b₁ holds
b₁ .labeledE() c= (b₁ .labelEdge b₂,b₃) .labeledE()

proof end;

theorem Th54: :: GLIB_003:54

for b₁ being finite EGraph
for b₂, b₃ being set st b₂ in the_Edges_of b₁ & not b₂ in b₁ .labeledE() holds
card ((b₁ .labelEdge b₂,b₃) .labeledE() ) = (card (b₁ .labeledE() )) + 1

proof end;

theorem Th55: :: GLIB_003:55

for b₁ being EGraph
for b₂, b₃, b₄ being set st not b₃ in b₁ .labeledE() & b₃ in (b₁ .labelEdge b₂,b₄) .labeledE() holds
( b₂ = b₃ & b₂ in the_Edges_of b₁ )

proof end;

theorem Th56: :: GLIB_003:56

for b₁ being EVGraph
for b₂, b₃ being set holds b₁ .labeledE() = (b₁ .labelVertex b₂,b₃) .labeledE() by Th49;

theorem Th57: :: GLIB_003:57

for b₁ being EGraph
for b₂, b₃ being set st b₂ in the_Edges_of b₁ holds
b₂ in (b₁ .labelEdge b₂,b₃) .labeledE()

proof end;

theorem Th58: :: GLIB_003:58

for b₁, b₂ being VGraph st the_VLabel_of b₁ = the_VLabel_of b₂ holds
b₁ .labeledV() = b₂ .labeledV() ;

theorem Th59: :: GLIB_003:59

for b₁ being VGraph
for b₂, b₃ being set st b₂ in the_Vertices_of b₁ holds
(b₁ .labelVertex b₂,b₃) .labeledV() = (b₁ .labeledV() ) \/ {b₂}

proof end;

theorem Th60: :: GLIB_003:60

for b₁ being VGraph
for b₂, b₃ being set st b₂ in the_Vertices_of b₁ holds
b₁ .labeledV() c= (b₁ .labelVertex b₂,b₃) .labeledV()

proof end;

theorem Th61: :: GLIB_003:61

for b₁ being finite VGraph
for b₂, b₃ being set st b₂ in the_Vertices_of b₁ & not b₂ in b₁ .labeledV() holds
card ((b₁ .labelVertex b₂,b₃) .labeledV() ) = (card (b₁ .labeledV() )) + 1

proof end;

theorem Th62: :: GLIB_003:62

for b₁ being VGraph
for b₂, b₃, b₄ being set st not b₃ in b₁ .labeledV() & b₃ in (b₁ .labelVertex b₂,b₄) .labeledV() holds
( b₂ = b₃ & b₂ in the_Vertices_of b₁ )

proof end;

theorem Th63: :: GLIB_003:63

for b₁ being EVGraph
for b₂, b₃ being set holds b₁ .labeledV() = (b₁ .labelEdge b₂,b₃) .labeledV() by Th43;

theorem Th64: :: GLIB_003:64

for b₁ being VGraph
for b₂ being Vertex of b₁
for b₃ being set holds b₂ in (b₁ .labelVertex b₂,b₃) .labeledV()

proof end;