:: Weighted and Labeled Graphs
:: by Gilbert Lee
::
:: Copyright (c) 2005-2021 Association of Mizar Users

definition
let D be set ;
let fs be FinSequence of D;
let fss be Subset of fs;
:: original: Seq
redefine func Seq fss -> FinSequence of D;
correctness
coherence
Seq fss is FinSequence of D
;
proof end;
end;

theorem :: GLIB_003:1
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being set
for p being FinSequence st p = ((((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*> holds
( len p = 10 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 & p . 8 = x8 & p . 9 = x9 & p . 10 = x10 )
proof end;

theorem Th2: :: GLIB_003:2
for fs being FinSequence of REAL
for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds
0 <= fs . i ) holds
Sum (Seq fss) <= Sum fs
proof end;

definition
func WeightSelector -> Element of NAT equals :: GLIB_003:def 1
5;
coherence
5 is Element of NAT
;
func ELabelSelector -> Element of NAT equals :: GLIB_003:def 2
6;
coherence
6 is Element of NAT
;
func VLabelSelector -> Element of NAT equals :: GLIB_003:def 3
7;
coherence
7 is Element of NAT
;
end;

:: deftheorem defines WeightSelector GLIB_003:def 1 :

:: deftheorem defines ELabelSelector GLIB_003:def 2 :

:: deftheorem defines VLabelSelector GLIB_003:def 3 :

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

:: deftheorem Def4 defines [Weighted] GLIB_003:def 4 :
for G being GraphStruct holds
( G is [Weighted] iff ( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G ) );

:: deftheorem Def5 defines [ELabeled] GLIB_003:def 5 :
for G being GraphStruct holds
( G is [ELabeled] iff ( ELabelSelector in dom G & ex f being Function st
( G . ELabelSelector = f & dom f c= the_Edges_of G ) ) );

:: deftheorem Def6 defines [VLabeled] GLIB_003:def 6 :
for G being GraphStruct holds
( G is [VLabeled] iff ( VLabelSelector in dom G & ex f being Function st
( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ) );

registration
existence
ex b1 being GraphStruct st
( b1 is [Graph-like] & b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )
proof end;
end;

definition end;

definition
let G be WGraph;
coherence by Def4;
end;

:: deftheorem defines the_Weight_of GLIB_003:def 7 :
for G being WGraph holds the_Weight_of G = G . WeightSelector;

definition
let G be EGraph;
coherence
proof end;
end;

:: deftheorem defines the_ELabel_of GLIB_003:def 8 :
for G being EGraph holds the_ELabel_of G = G . ELabelSelector;

definition
let G be VGraph;
coherence
proof end;
end;

:: deftheorem defines the_VLabel_of GLIB_003:def 9 :
for G being VGraph holds the_VLabel_of G = G . VLabelSelector;

Lm1: for G being EGraph holds dom () c= the_Edges_of G
proof end;

Lm2: for G being VGraph holds dom () c= the_Vertices_of G
proof end;

registration
let G be _Graph;
let X be set ;
coherence
G .set (WeightSelector,X) is [Graph-like]
proof end;
coherence
G .set (ELabelSelector,X) is [Graph-like]
proof end;
coherence
G .set (VLabelSelector,X) is [Graph-like]
proof end;
end;

Lm3: for G being _Graph
for X being set holds
( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G )

proof end;

registration
let G be _finite _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> _finite ;
coherence
G .set (WeightSelector,X) is _finite
proof end;
cluster G .set (ELabelSelector,X) -> _finite ;
coherence
G .set (ELabelSelector,X) is _finite
proof end;
cluster G .set (VLabelSelector,X) -> _finite ;
coherence
G .set (VLabelSelector,X) is _finite
proof end;
end;

registration
let G be loopless _Graph;
let X be set ;
coherence
G .set (WeightSelector,X) is loopless
proof end;
coherence
G .set (ELabelSelector,X) is loopless
proof end;
coherence
G .set (VLabelSelector,X) is loopless
proof end;
end;

registration
let G be _trivial _Graph;
let X be set ;
coherence
G .set (WeightSelector,X) is _trivial
proof end;
coherence
G .set (ELabelSelector,X) is _trivial
proof end;
coherence
G .set (VLabelSelector,X) is _trivial
proof end;
end;

registration
let G be non _trivial _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> non _trivial ;
coherence
not G .set (WeightSelector,X) is _trivial
proof end;
cluster G .set (ELabelSelector,X) -> non _trivial ;
coherence
not G .set (ELabelSelector,X) is _trivial
proof end;
cluster G .set (VLabelSelector,X) -> non _trivial ;
coherence
not G .set (VLabelSelector,X) is _trivial
proof end;
end;

registration
let G be non-multi _Graph;
let X be set ;
coherence
G .set (WeightSelector,X) is non-multi
proof end;
coherence
G .set (ELabelSelector,X) is non-multi
proof end;
coherence
G .set (VLabelSelector,X) is non-multi
proof end;
end;

registration
let G be non-Dmulti _Graph;
let X be set ;
coherence
G .set (WeightSelector,X) is non-Dmulti
proof end;
coherence
G .set (ELabelSelector,X) is non-Dmulti
proof end;
coherence
G .set (VLabelSelector,X) is non-Dmulti
proof end;
end;

registration
let G be connected _Graph;
let X be set ;
coherence
G .set (WeightSelector,X) is connected
proof end;
coherence
G .set (ELabelSelector,X) is connected
proof end;
coherence
G .set (VLabelSelector,X) is connected
proof end;
end;

registration
let G be acyclic _Graph;
let X be set ;
cluster G .set (WeightSelector,X) -> acyclic ;
coherence
G .set (WeightSelector,X) is acyclic
proof end;
cluster G .set (ELabelSelector,X) -> acyclic ;
coherence
G .set (ELabelSelector,X) is acyclic
proof end;
cluster G .set (VLabelSelector,X) -> acyclic ;
coherence
G .set (VLabelSelector,X) is acyclic
proof end;
end;

registration
let G be WGraph;
let X be set ;
coherence
G .set (ELabelSelector,X) is [Weighted]
proof end;
coherence
G .set (VLabelSelector,X) is [Weighted]
proof end;
end;

registration
let G be _Graph;
let X be ManySortedSet of the_Edges_of G;
coherence
G .set (WeightSelector,X) is [Weighted]
proof end;
end;

registration
let G be _Graph;
let WL be non empty set ;
let W be Function of (),WL;
coherence
G .set (WeightSelector,W) is [Weighted]
;
end;

registration
let G be EGraph;
let X be set ;
coherence
G .set (WeightSelector,X) is [ELabeled]
proof end;
coherence
G .set (VLabelSelector,X) is [ELabeled]
proof end;
end;

registration
let G be _Graph;
let Y be set ;
let X be PartFunc of (),Y;
coherence
G .set (ELabelSelector,X) is [ELabeled]
proof end;
end;

registration
let G be _Graph;
let X be ManySortedSet of the_Edges_of G;
coherence
G .set (ELabelSelector,X) is [ELabeled]
proof end;
end;

registration
let G be VGraph;
let X be set ;
coherence
G .set (WeightSelector,X) is [VLabeled]
proof end;
coherence
G .set (ELabelSelector,X) is [VLabeled]
proof end;
end;

registration
let G be _Graph;
let Y be set ;
let X be PartFunc of (),Y;
coherence
G .set (VLabelSelector,X) is [VLabeled]
proof end;
end;

registration
let G be _Graph;
let X be ManySortedSet of the_Vertices_of G;
coherence
G .set (VLabelSelector,X) is [VLabeled]
proof end;
end;

registration
let G be _Graph;
coherence
proof end;
coherence
proof end;
end;

registration
let G be _Graph;
existence
ex b1 being Subgraph of G st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )
proof end;
end;

definition
let G be WGraph;
let G2 be [Weighted] Subgraph of G;
attr G2 is weight-inheriting means :Def10: :: GLIB_003:def 10
the_Weight_of G2 = () | ();
end;

:: deftheorem Def10 defines weight-inheriting GLIB_003:def 10 :
for G being WGraph
for G2 being [Weighted] Subgraph of G holds
( G2 is weight-inheriting iff the_Weight_of G2 = () | () );

definition
let G be EGraph;
let G2 be [ELabeled] Subgraph of G;
attr G2 is elabel-inheriting means :Def11: :: GLIB_003:def 11
the_ELabel_of G2 = () | ();
end;

:: deftheorem Def11 defines elabel-inheriting GLIB_003:def 11 :
for G being EGraph
for G2 being [ELabeled] Subgraph of G holds
( G2 is elabel-inheriting iff the_ELabel_of G2 = () | () );

definition
let G be VGraph;
let G2 be [VLabeled] Subgraph of G;
attr G2 is vlabel-inheriting means :Def12: :: GLIB_003:def 12
the_VLabel_of G2 = () | ();
end;

:: deftheorem Def12 defines vlabel-inheriting GLIB_003:def 12 :
for G being VGraph
for G2 being [VLabeled] Subgraph of G holds
( G2 is vlabel-inheriting iff the_VLabel_of G2 = () | () );

registration
let G be WGraph;
existence
ex b1 being [Weighted] Subgraph of G st b1 is weight-inheriting
proof end;
end;

registration
let G be EGraph;
existence
ex b1 being [ELabeled] Subgraph of G st b1 is elabel-inheriting
proof end;
end;

registration
let G be VGraph;
existence
ex b1 being [VLabeled] Subgraph of G st b1 is vlabel-inheriting
proof end;
end;

registration
let G be WEGraph;
existence
ex b1 being [Weighted] [ELabeled] Subgraph of G st
( b1 is weight-inheriting & b1 is elabel-inheriting )
proof end;
end;

registration
let G be WVGraph;
existence
ex b1 being [Weighted] [VLabeled] Subgraph of G st
( b1 is weight-inheriting & b1 is vlabel-inheriting )
proof end;
end;

registration
let G be EVGraph;
existence
ex b1 being [ELabeled] [VLabeled] Subgraph of G st
( b1 is elabel-inheriting & b1 is vlabel-inheriting )
proof end;
end;

registration
let G be WEVGraph;
existence
ex b1 being [Weighted] [ELabeled] [VLabeled] Subgraph of G st
( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting )
proof end;
end;

definition end;

definition end;

definition end;

definition end;

definition end;

definition end;

definition end;

registration
let G be _Graph;
let V, E be set ;
existence
ex b1 being inducedSubgraph of G,V,E st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )
proof end;
end;

registration
let G be WGraph;
let V, E be set ;
existence
ex b1 being [Weighted] inducedSubgraph of G,V,E st b1 is weight-inheriting
proof end;
end;

registration
let G be EGraph;
let V, E be set ;
existence
ex b1 being [ELabeled] inducedSubgraph of G,V,E st b1 is elabel-inheriting
proof end;
end;

registration
let G be VGraph;
let V, E be set ;
existence
ex b1 being [VLabeled] inducedSubgraph of G,V,E st b1 is vlabel-inheriting
proof end;
end;

registration
let G be WEGraph;
let V, E be set ;
existence
ex b1 being [Weighted] [ELabeled] inducedSubgraph of G,V,E st
( b1 is weight-inheriting & b1 is elabel-inheriting )
proof end;
end;

registration
let G be WVGraph;
let V, E be set ;
existence
ex b1 being [Weighted] [VLabeled] inducedSubgraph of G,V,E st
( b1 is weight-inheriting & b1 is vlabel-inheriting )
proof end;
end;

registration
let G be EVGraph;
let V, E be set ;
existence
ex b1 being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b1 is elabel-inheriting & b1 is vlabel-inheriting )
proof end;
end;

registration
let G be WEVGraph;
let V, E be set ;
existence
ex b1 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting )
proof end;
end;

definition
let G be WGraph;
let V, E be set ;
mode inducedWSubgraph of G,V,E is [Weighted] weight-inheriting inducedSubgraph of G,V,E;
end;

definition
let G be EGraph;
let V, E be set ;
mode inducedESubgraph of G,V,E is [ELabeled] elabel-inheriting inducedSubgraph of G,V,E;
end;

definition
let G be VGraph;
let V, E be set ;
mode inducedVSubgraph of G,V,E is [VLabeled] vlabel-inheriting inducedSubgraph of G,V,E;
end;

definition end;

definition end;

definition end;

definition end;

definition
let G be WGraph;
let V be set ;
mode inducedWSubgraph of G,V is inducedWSubgraph of G,V,G .edgesBetween V;
end;

definition
let G be EGraph;
let V be set ;
mode inducedESubgraph of G,V is inducedESubgraph of G,V,G .edgesBetween V;
end;

definition
let G be VGraph;
let V be set ;
mode inducedVSubgraph of G,V is inducedVSubgraph of G,V,G .edgesBetween V;
end;

definition
let G be WEGraph;
let V be set ;
mode inducedWESubgraph of G,V is inducedWESubgraph of G,V,G .edgesBetween V;
end;

definition
let G be WVGraph;
let V be set ;
mode inducedWVSubgraph of G,V is inducedWVSubgraph of G,V,G .edgesBetween V;
end;

definition
let G be EVGraph;
let V be set ;
mode inducedEVSubgraph of G,V is inducedEVSubgraph of G,V,G .edgesBetween V;
end;

definition
let G be WEVGraph;
let V be set ;
mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G,V,G .edgesBetween V;
end;

definition
let G be WGraph;
attr G is real-weighted means :Def13: :: GLIB_003:def 13
the_Weight_of G is real-valued ;
end;

:: deftheorem Def13 defines real-weighted GLIB_003:def 13 :
for G being WGraph holds
( G is real-weighted iff the_Weight_of G is real-valued );

definition
let G be WGraph;
attr G is nonnegative-weighted means :Def14: :: GLIB_003:def 14
rng () c= Real>=0 ;
end;

:: deftheorem Def14 defines nonnegative-weighted GLIB_003:def 14 :
for G being WGraph holds
( G is nonnegative-weighted iff rng () c= Real>=0 );

registration
coherence
for b1 being WGraph st b1 is nonnegative-weighted holds
b1 is real-weighted
by ;
end;

definition
let G be EGraph;
attr G is real-elabeled means :Def15: :: GLIB_003:def 15
the_ELabel_of G is real-valued ;
end;

:: deftheorem Def15 defines real-elabeled GLIB_003:def 15 :
for G being EGraph holds
( G is real-elabeled iff the_ELabel_of G is real-valued );

definition
let G be VGraph;
attr G is real-vlabeled means :Def16: :: GLIB_003:def 16
the_VLabel_of G is real-valued ;
end;

:: deftheorem Def16 defines real-vlabeled GLIB_003:def 16 :
for G being VGraph holds
( G is real-vlabeled iff the_VLabel_of G is real-valued );

definition
let G be WEVGraph;
attr G is real-WEV means :: GLIB_003:def 17
( G is real-weighted & G is real-elabeled & G is real-vlabeled );
end;

:: deftheorem defines real-WEV GLIB_003:def 17 :
for G being WEVGraph holds
( G is real-WEV iff ( G is real-weighted & G is real-elabeled & G is real-vlabeled ) );

registration
coherence
for b1 being WEVGraph st b1 is real-WEV holds
( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled )
;
coherence
for b1 being WEVGraph st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds
b1 is real-WEV
;
end;

registration
let G be _Graph;
let X be Function of (),REAL;
coherence
G .set (WeightSelector,X) is real-weighted
by GLIB_000:8;
end;

registration
let G be _Graph;
let X be PartFunc of (),REAL;
coherence
G .set (ELabelSelector,X) is real-elabeled
by GLIB_000:8;
end;

registration
let G be _Graph;
let X be real-valued ManySortedSet of the_Edges_of G;
coherence
G .set (ELabelSelector,X) is real-elabeled
by GLIB_000:8;
end;

registration
let G be _Graph;
let X be PartFunc of (),REAL;
coherence
G .set (VLabelSelector,X) is real-vlabeled
by GLIB_000:8;
end;

registration
let G be _Graph;
let X be real-valued ManySortedSet of the_Vertices_of G;
coherence
G .set (VLabelSelector,X) is real-vlabeled
by GLIB_000:8;
end;

registration
let G be _Graph;
coherence
proof end;
coherence
proof end;
end;

registration
let G be _Graph;
let v be Vertex of G;
let val be Real;
cluster G .set (VLabelSelector,(v .--> val)) -> [VLabeled] ;
coherence
G .set (VLabelSelector,(v .--> val)) is [VLabeled]
proof end;
end;

registration
let G be _Graph;
let v be Vertex of G;
let val be Real;
cluster G .set (VLabelSelector,(v .--> val)) -> real-vlabeled ;
coherence
G .set (VLabelSelector,(v .--> val)) is real-vlabeled
proof end;
end;

registration
existence
ex b1 being WEVGraph st
( b1 is _finite & b1 is _trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV )
proof end;
existence
ex b1 being WEVGraph st
( b1 is _finite & not b1 is _trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV )
proof end;
end;

registration
let G be _finite WGraph;
coherence
proof end;
end;

registration
let G be _finite EGraph;
coherence
proof end;
end;

registration
let G be _finite VGraph;
coherence
proof end;
end;

registration
let G be real-weighted WGraph;
coherence by Def13;
end;

registration
let G be real-elabeled EGraph;
coherence by Def15;
end;

registration
let G be real-vlabeled VGraph;
coherence by Def16;
end;

registration
let G be real-weighted WGraph;
let X be set ;
coherence
G .set (ELabelSelector,X) is real-weighted
proof end;
coherence
G .set (VLabelSelector,X) is real-weighted
proof end;
end;

registration
let G be nonnegative-weighted WGraph;
let X be set ;
coherence
proof end;
coherence
proof end;
end;

registration
let G be real-elabeled EGraph;
let X be set ;
coherence
G .set (WeightSelector,X) is real-elabeled
proof end;
coherence
G .set (VLabelSelector,X) is real-elabeled
proof end;
end;

registration
let G be real-vlabeled VGraph;
let X be set ;
coherence
G .set (WeightSelector,X) is real-vlabeled
proof end;
coherence
G .set (ELabelSelector,X) is real-vlabeled
proof end;
end;

definition
let G be WGraph;
let W be Walk of G;
func W .weightSeq() -> FinSequence means :Def18: :: GLIB_003:def 18
( len it = len () & ( for n being Nat st 1 <= n & n <= len it holds
it . n = () . (() . n) ) );
existence
ex b1 being FinSequence st
( len b1 = len () & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = () . (() . n) ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = len () & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = () . (() . n) ) & len b2 = len () & ( for n being Nat st 1 <= n & n <= len b2 holds
b2 . n = () . (() . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :
for G being WGraph
for W being Walk of G
for b3 being FinSequence holds
( b3 = W .weightSeq() iff ( len b3 = len () & ( for n being Nat st 1 <= n & n <= len b3 holds
b3 . n = () . (() . n) ) ) );

definition
let G be real-weighted WGraph;
let W be Walk of G;
:: original: .weightSeq()
redefine func W .weightSeq() -> FinSequence of REAL ;
coherence
proof end;
end;

definition
let G be real-weighted WGraph;
let W be Walk of G;
func W .cost() -> Real equals :: GLIB_003:def 19
Sum ();
coherence
Sum () is Real
;
end;

:: deftheorem defines .cost() GLIB_003:def 19 :
for G being real-weighted WGraph
for W being Walk of G holds W .cost() = Sum ();

Lm4: for x, y, X, Y being set
for f being PartFunc of X,Y st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y

proof end;

definition
let G be EGraph;
func G .labeledE() -> Subset of () equals :: GLIB_003:def 20
dom ();
coherence
dom () is Subset of ()
by Lm1;
end;

:: deftheorem defines .labeledE() GLIB_003:def 20 :
for G being EGraph holds G .labeledE() = dom ();

definition
let G be EGraph;
let e, x be object ;
func G .labelEdge (e,x) -> EGraph equals :Def21: :: GLIB_003:def 21
G .set (ELabelSelector,(() +* (e .--> x))) if e in the_Edges_of G
otherwise G;
coherence
( ( e in the_Edges_of G implies G .set (ELabelSelector,(() +* (e .--> x))) is EGraph ) & ( not e in the_Edges_of G implies G is EGraph ) )
proof end;
consistency
for b1 being EGraph holds verum
;
end;

:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :
for G being EGraph
for e, x being object holds
( ( e in the_Edges_of G implies G .labelEdge (e,x) = G .set (ELabelSelector,(() +* (e .--> x))) ) & ( not e in the_Edges_of G implies G .labelEdge (e,x) = G ) );

registration
let G be _finite EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> _finite ;
coherence
G .labelEdge (e,x) is _finite
proof end;
end;

registration
let G be loopless EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> loopless ;
coherence
G .labelEdge (e,x) is loopless
proof end;
end;

registration
let G be _trivial EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> _trivial ;
coherence
G .labelEdge (e,x) is _trivial
proof end;
end;

registration
let G be non _trivial EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> non _trivial ;
coherence
not G .labelEdge (e,x) is _trivial
proof end;
end;

registration
let G be non-multi EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> non-multi ;
coherence
G .labelEdge (e,x) is non-multi
proof end;
end;

registration
let G be non-Dmulti EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> non-Dmulti ;
coherence
G .labelEdge (e,x) is non-Dmulti
proof end;
end;

registration
let G be connected EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> connected ;
coherence
G .labelEdge (e,x) is connected
proof end;
end;

registration
let G be acyclic EGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> acyclic ;
coherence
G .labelEdge (e,x) is acyclic
proof end;
end;

registration
let G be WEGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> [Weighted] ;
coherence
G .labelEdge (e,x) is [Weighted]
proof end;
end;

registration
let G be EVGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> [VLabeled] ;
coherence
G .labelEdge (e,x) is [VLabeled]
proof end;
end;

registration
let G be real-weighted WEGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> real-weighted ;
coherence
G .labelEdge (e,x) is real-weighted
proof end;
end;

registration
let G be nonnegative-weighted WEGraph;
let e, x be set ;
coherence
G .labelEdge (e,x) is nonnegative-weighted
proof end;
end;

registration
let G be real-elabeled EGraph;
let e be set ;
let x be Real;
cluster G .labelEdge (e,x) -> real-elabeled ;
coherence
G .labelEdge (e,x) is real-elabeled
proof end;
end;

registration
let G be real-vlabeled EVGraph;
let e, x be set ;
cluster G .labelEdge (e,x) -> real-vlabeled ;
coherence
G .labelEdge (e,x) is real-vlabeled
proof end;
end;

definition
let G be VGraph;
let v, x be object ;
func G .labelVertex (v,x) -> VGraph equals :Def22: :: GLIB_003:def 22
G .set (VLabelSelector,(() +* (v .--> x))) if v in the_Vertices_of G
otherwise G;
coherence
( ( v in the_Vertices_of G implies G .set (VLabelSelector,(() +* (v .--> x))) is VGraph ) & ( not v in the_Vertices_of G implies G is VGraph ) )
proof end;
consistency
for b1 being VGraph holds verum
;
end;

:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :
for G being VGraph
for v, x being object holds
( ( v in the_Vertices_of G implies G .labelVertex (v,x) = G .set (VLabelSelector,(() +* (v .--> x))) ) & ( not v in the_Vertices_of G implies G .labelVertex (v,x) = G ) );

definition
let G be VGraph;
func G .labeledV() -> Subset of () equals :: GLIB_003:def 23
dom ();
coherence
dom () is Subset of ()
by Lm2;
end;

:: deftheorem defines .labeledV() GLIB_003:def 23 :
for G being VGraph holds G .labeledV() = dom ();

registration
let G be _finite VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> _finite ;
coherence
G .labelVertex (v,x) is _finite
proof end;
end;

registration
let G be loopless VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> loopless ;
coherence
G .labelVertex (v,x) is loopless
proof end;
end;

registration
let G be _trivial VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> _trivial ;
coherence
G .labelVertex (v,x) is _trivial
proof end;
end;

registration
let G be non _trivial VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> non _trivial ;
coherence
not G .labelVertex (v,x) is _trivial
proof end;
end;

registration
let G be non-multi VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> non-multi ;
coherence
G .labelVertex (v,x) is non-multi
proof end;
end;

registration
let G be non-Dmulti VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> non-Dmulti ;
coherence
G .labelVertex (v,x) is non-Dmulti
proof end;
end;

registration
let G be connected VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> connected ;
coherence
G .labelVertex (v,x) is connected
proof end;
end;

registration
let G be acyclic VGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> acyclic ;
coherence
G .labelVertex (v,x) is acyclic
proof end;
end;

registration
let G be WVGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> [Weighted] ;
coherence
G .labelVertex (v,x) is [Weighted]
proof end;
end;

registration
let G be EVGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> [ELabeled] ;
coherence
G .labelVertex (v,x) is [ELabeled]
proof end;
end;

registration
let G be real-weighted WVGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> real-weighted ;
coherence
G .labelVertex (v,x) is real-weighted
proof end;
end;

registration
let G be nonnegative-weighted WVGraph;
let v, x be set ;
coherence
G .labelVertex (v,x) is nonnegative-weighted
proof end;
end;

registration
let G be real-elabeled EVGraph;
let v, x be set ;
cluster G .labelVertex (v,x) -> real-elabeled ;
coherence
G .labelVertex (v,x) is real-elabeled
proof end;
end;

registration
let G be real-vlabeled VGraph;
let v be set ;
let x be Real;
cluster G .labelVertex (v,x) -> real-vlabeled ;
coherence
G .labelVertex (v,x) is real-vlabeled
proof end;
end;

registration
let G be real-weighted WGraph;
coherence
for b1 being WSubgraph of G holds b1 is real-weighted
proof end;
end;

registration
let G be nonnegative-weighted WGraph;
coherence
for b1 being WSubgraph of G holds b1 is nonnegative-weighted
proof end;
end;

registration
let G be real-elabeled EGraph;
coherence
for b1 being ESubgraph of G holds b1 is real-elabeled
proof end;
end;

registration
let G be real-vlabeled VGraph;
coherence
for b1 being VSubgraph of G holds b1 is real-vlabeled
proof end;
end;

definition
let GSq be GraphSeq;
attr GSq is [Weighted] means :Def24: :: GLIB_003:def 24
for x being Nat holds GSq . x is [Weighted] ;
attr GSq is [ELabeled] means :Def25: :: GLIB_003:def 25
for x being Nat holds GSq . x is [ELabeled] ;
attr GSq is [VLabeled] means :Def26: :: GLIB_003:def 26
for x being Nat holds GSq . x is [VLabeled] ;
end;

:: deftheorem Def24 defines [Weighted] GLIB_003:def 24 :
for GSq being GraphSeq holds
( GSq is [Weighted] iff for x being Nat holds GSq . x is [Weighted] );

:: deftheorem Def25 defines [ELabeled] GLIB_003:def 25 :
for GSq being GraphSeq holds
( GSq is [ELabeled] iff for x being Nat holds GSq . x is [ELabeled] );

:: deftheorem Def26 defines [VLabeled] GLIB_003:def 26 :
for GSq being GraphSeq holds
( GSq is [VLabeled] iff for x being Nat holds GSq . x is [VLabeled] );

registration
existence
ex b1 being GraphSeq st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )
proof end;
end;

registration
let GSq be WGraphSeq;
let x be Nat;
cluster GSq . x -> [Weighted] for _Graph;
coherence
for b1 being _Graph st b1 = GSq . x holds
b1 is [Weighted]
by Def24;
end;

registration
let GSq be EGraphSeq;
let x be Nat;
cluster GSq . x -> [ELabeled] for _Graph;
coherence
for b1 being _Graph st b1 = GSq . x holds
b1 is [ELabeled]
by Def25;
end;

registration
let GSq be VGraphSeq;
let x be Nat;
cluster GSq . x -> [VLabeled] for _Graph;
coherence
for b1 being _Graph st b1 = GSq . x holds
b1 is [VLabeled]
by Def26;
end;

definition
let GSq be WGraphSeq;
attr GSq is real-weighted means :Def27: :: GLIB_003:def 27
for x being Nat holds GSq . x is real-weighted ;
attr GSq is nonnegative-weighted means :Def28: :: GLIB_003:def 28
for x being Nat holds GSq . x is nonnegative-weighted ;
end;

:: deftheorem Def27 defines real-weighted GLIB_003:def 27 :
for GSq being WGraphSeq holds
( GSq is real-weighted iff for x being Nat holds GSq . x is real-weighted );

:: deftheorem Def28 defines nonnegative-weighted GLIB_003:def 28 :
for GSq being WGraphSeq holds
( GSq is nonnegative-weighted iff for x being Nat holds GSq . x is nonnegative-weighted );

definition
let GSq be EGraphSeq;
attr GSq is real-elabeled means :Def29: :: GLIB_003:def 29
for x being Nat holds GSq . x is real-elabeled ;
end;

:: deftheorem Def29 defines real-elabeled GLIB_003:def 29 :
for GSq being EGraphSeq holds
( GSq is real-elabeled iff for x being Nat holds GSq . x is real-elabeled );

definition
let GSq be VGraphSeq;
attr GSq is real-vlabeled means :Def30: :: GLIB_003:def 30
for x being Nat holds GSq . x is real-vlabeled ;
end;

:: deftheorem Def30 defines real-vlabeled GLIB_003:def 30 :
for GSq being VGraphSeq holds
( GSq is real-vlabeled iff for x being Nat holds GSq . x is real-vlabeled );

definition
let GSq be WEVGraphSeq;
attr GSq is real-WEV means :: GLIB_003:def 31
for x being Nat holds GSq . x is real-WEV ;
end;

:: deftheorem defines real-WEV GLIB_003:def 31 :
for GSq being WEVGraphSeq holds
( GSq is real-WEV iff for x being Nat holds GSq . x is real-WEV );

registration
coherence
for b1 being WEVGraphSeq st b1 is real-WEV holds
( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled )
proof end;
coherence
for b1 being WEVGraphSeq st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds
b1 is real-WEV
proof end;
end;

registration
existence
ex b1 being WEVGraphSeq st
( b1 is halting & b1 is _finite & b1 is loopless & b1 is _trivial & b1 is non-multi & b1 is simple & b1 is real-WEV & b1 is nonnegative-weighted & b1 is Tree-like )
proof end;
end;

registration
let GSq be real-weighted WGraphSeq;
let x be Nat;
cluster GSq . x -> real-weighted for WGraph;
coherence
for b1 being WGraph st b1 = GSq . x holds
b1 is real-weighted
by Def27;
end;

registration
let GSq be nonnegative-weighted WGraphSeq;
let x be Nat;
cluster GSq . x -> nonnegative-weighted for WGraph;
coherence
for b1 being WGraph st b1 = GSq . x holds
b1 is nonnegative-weighted
by Def28;
end;

registration
let GSq be real-elabeled EGraphSeq;
let x be Nat;
cluster GSq . x -> real-elabeled for EGraph;
coherence
for b1 being EGraph st b1 = GSq . x holds
b1 is real-elabeled
by Def29;
end;

registration
let GSq be real-vlabeled VGraphSeq;
let x be Nat;
cluster GSq . x -> real-vlabeled for VGraph;
coherence
for b1 being VGraph st b1 = GSq . x holds
b1 is real-vlabeled
by Def30;
end;

theorem :: GLIB_003:3
( WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7 ) ;

theorem :: GLIB_003:4
( ( for G being WGraph holds the_Weight_of G = G . WeightSelector ) & ( for G being EGraph holds the_ELabel_of G = G . ELabelSelector ) & ( for G being VGraph holds the_VLabel_of G = G . VLabelSelector ) ) ;

theorem :: GLIB_003:5
for G being EGraph holds dom () c= the_Edges_of G by Lm1;

theorem :: GLIB_003:6
for G being VGraph holds dom () c= the_Vertices_of G by Lm2;

:: Theorems regarding G.set()
theorem :: GLIB_003:7
for G being _Graph
for X being set holds
( G == G .set (WeightSelector,X) & G == G .set (ELabelSelector,X) & G == G .set (VLabelSelector,X) ) by Lm3;

:: Theorems regarding WSubgraphs
theorem :: GLIB_003:8
for G1, G2, G3 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 holds
G2 is WSubgraph of G3
proof end;

theorem :: GLIB_003:9
for G1 being WGraph
for G2 being WSubgraph of G1
for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1
proof end;

theorem :: GLIB_003:10
for G1, G2 being WGraph
for G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds
G3 is WSubgraph of G2
proof end;

theorem :: GLIB_003:11
for G1 being WGraph
for G2 being WSubgraph of G1
for x being set st x in the_Edges_of G2 holds
() . x = () . x
proof end;

:: Theorems regarding W.weightSeq()
theorem Th12: :: GLIB_003:12
for G being WGraph
for W being Walk of G st W is V5() holds
W .weightSeq() = {}
proof end;

theorem :: GLIB_003:13
for G being WGraph
for W being Walk of G holds len () = W .length()
proof end;

theorem Th14: :: GLIB_003:14
for G being WGraph
for x, y, e being set st e Joins x,y,G holds
(G .walkOf (x,e,y)) .weightSeq() = <*(() . e)*>
proof end;

theorem Th15: :: GLIB_003:15
for G being WGraph
for W being Walk of G holds () .weightSeq() = Rev ()
proof end;

theorem Th16: :: GLIB_003:16
for G being WGraph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .weightSeq() = () ^ ()
proof end;

theorem Th17: :: GLIB_003:17
for G being WGraph
for W being Walk of G
for e being set st e in () .edgesInOut() holds
(W .addEdge e) .weightSeq() = () ^ <*(() . e)*>
proof end;

theorem Th18: :: GLIB_003:18
for G being real-weighted WGraph
for W1 being Walk of G
for W2 being Subwalk of W1 ex ws being Subset of () st W2 .weightSeq() = Seq ws
proof end;

theorem Th19: :: GLIB_003:19
for G1, G2 being WGraph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds
W1 .weightSeq() = W2 .weightSeq()
proof end;

theorem Th20: :: GLIB_003:20
for G1 being WGraph
for G2 being WSubgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .weightSeq() = W2 .weightSeq()
proof end;

:: Theorems regarding W.cost()
theorem :: GLIB_003:21
for G being real-weighted WGraph
for W being Walk of G st W is V5() holds
W .cost() = 0 by ;

theorem :: GLIB_003:22
for G being real-weighted WGraph
for v1, v2 being Vertex of G
for e being set st e Joins v1,v2,G holds
(G .walkOf (v1,e,v2)) .cost() = () . e
proof end;

theorem :: GLIB_003:23
for G being real-weighted WGraph
for W being Walk of G holds W .cost() = () .cost()
proof end;

theorem :: GLIB_003:24
for G being real-weighted WGraph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost())
proof end;

theorem :: GLIB_003:25
for G being real-weighted WGraph
for W being Walk of G
for e being set st e in () .edgesInOut() holds
(W .addEdge e) .cost() = () + (() . e)
proof end;

theorem :: GLIB_003:26
for G1, G2 being real-weighted WGraph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds
W1 .cost() = W2 .cost() by Th19;

theorem :: GLIB_003:27
for G1 being real-weighted WGraph
for G2 being WSubgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .cost() = W2 .cost() by Th20;

:: Theorems regarding nonnegative-weighted WGraphs
theorem Th28: :: GLIB_003:28
for G being nonnegative-weighted WGraph
for W being Walk of G
for n being Element of NAT st n in dom () holds
0 <= () . n
proof end;

theorem :: GLIB_003:29
for G being nonnegative-weighted WGraph
for W being Walk of G holds 0 <= W .cost()
proof end;

theorem :: GLIB_003:30
for G being nonnegative-weighted WGraph
for W1 being Walk of G
for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()
proof end;

theorem :: GLIB_003:31
for G being nonnegative-weighted WGraph
for e being set st e in the_Edges_of G holds
0 <= () . e
proof end;

:: Theorems involving G.labelEdge
theorem Th32: :: GLIB_003:32
for G being EGraph
for e, x being set st e in the_Edges_of G holds
the_ELabel_of (G .labelEdge (e,x)) = () +* (e .--> x)
proof end;

theorem :: GLIB_003:33
for G being EGraph
for e, x being set st e in the_Edges_of G holds
(the_ELabel_of (G .labelEdge (e,x))) . e = x
proof end;

theorem :: GLIB_003:34
for G being EGraph
for e, x being set holds G == G .labelEdge (e,x)
proof end;

theorem :: GLIB_003:35
for G being WEGraph
for e, x being set holds the_Weight_of G = the_Weight_of (G .labelEdge (e,x))
proof end;

theorem Th36: :: GLIB_003:36
for G being EVGraph
for e, x being set holds the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x))
proof end;

theorem :: GLIB_003:37
for G being EGraph
for e1, e2, x being set st e1 <> e2 holds
(the_ELabel_of (G .labelEdge (e1,x))) . e2 = () . e2
proof end;

:: Theorems involving G.labelVertex
theorem Th38: :: GLIB_003:38
for G being VGraph
for v, x being set st v in the_Vertices_of G holds
the_VLabel_of (G .labelVertex (v,x)) = () +* (v .--> x)
proof end;

theorem :: GLIB_003:39
for G being VGraph
for v, x being set st v in the_Vertices_of G holds
(the_VLabel_of (G .labelVertex (v,x))) . v = x
proof end;

theorem :: GLIB_003:40
for G being VGraph
for v, x being set holds G == G .labelVertex (v,x)
proof end;

theorem :: GLIB_003:41
for G being WVGraph
for v, x being set holds the_Weight_of G = the_Weight_of (G .labelVertex (v,x))
proof end;

theorem Th42: :: GLIB_003:42
for G being EVGraph
for v, x being set holds the_ELabel_of G = the_ELabel_of (G .labelVertex (v,x))
proof end;

theorem :: GLIB_003:43
for G being VGraph
for v1, v2, x being set st v1 <> v2 holds
(the_VLabel_of (G .labelVertex (v1,x))) . v2 = () . v2
proof end;

:: Theorems regarding G.labeledE()
theorem :: GLIB_003:44
for G1, G2 being EGraph st the_ELabel_of G1 = the_ELabel_of G2 holds
G1 .labeledE() = G2 .labeledE() ;

theorem Th45: :: GLIB_003:45
for G being EGraph
for e, x being set st e in the_Edges_of G holds
(G .labelEdge (e,x)) .labeledE() = () \/ {e}
proof end;

theorem :: GLIB_003:46
for G being EGraph
for e, x being set st e in the_Edges_of G holds
G .labeledE() c= (G .labelEdge (e,x)) .labeledE()
proof end;

theorem :: GLIB_003:47
for G being _finite EGraph
for e, x being set st e in the_Edges_of G & not e in G .labeledE() holds
card ((G .labelEdge (e,x)) .labeledE()) = (card ()) + 1
proof end;

theorem :: GLIB_003:48
for G being EGraph
for e1, e2, x being set st not e2 in G .labeledE() & e2 in (G .labelEdge (e1,x)) .labeledE() holds
( e1 = e2 & e1 in the_Edges_of G )
proof end;

theorem :: GLIB_003:49
for G being EVGraph
for v, x being set holds G .labeledE() = (G .labelVertex (v,x)) .labeledE() by Th42;

theorem :: GLIB_003:50
for G being EGraph
for e, x being set st e in the_Edges_of G holds
e in (G .labelEdge (e,x)) .labeledE()
proof end;

:: Theorems regarding G.labeledV()
theorem :: GLIB_003:51
for G1, G2 being VGraph st the_VLabel_of G1 = the_VLabel_of G2 holds
G1 .labeledV() = G2 .labeledV() ;

theorem Th52: :: GLIB_003:52
for G being VGraph
for v, x being set st v in the_Vertices_of G holds
(G .labelVertex (v,x)) .labeledV() = () \/ {v}
proof end;

theorem :: GLIB_003:53
for G being VGraph
for v, x being set st v in the_Vertices_of G holds
G .labeledV() c= (G .labelVertex (v,x)) .labeledV()
proof end;

theorem :: GLIB_003:54
for G being _finite VGraph
for v, x being set st v in the_Vertices_of G & not v in G .labeledV() holds
card ((G .labelVertex (v,x)) .labeledV()) = (card ()) + 1
proof end;

theorem :: GLIB_003:55
for G being VGraph
for v1, v2, x being set st not v2 in G .labeledV() & v2 in (G .labelVertex (v1,x)) .labeledV() holds
( v1 = v2 & v1 in the_Vertices_of G )
proof end;

theorem :: GLIB_003:56
for G being EVGraph
for e, x being set holds G .labeledV() = (G .labelEdge (e,x)) .labeledV() by Th36;

theorem :: GLIB_003:57
for G being VGraph
for v being Vertex of G
for x being set holds v in (G .labelVertex (v,x)) .labeledV()
proof end;