:: Weighted and Labeled Graphs
:: by Gilbert Lee
::
:: Received February 22, 2005
:: 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 :
WeightSelector = 5;

:: deftheorem defines ELabelSelector GLIB_003:def 2 :
ELabelSelector = 6;

:: deftheorem defines VLabelSelector GLIB_003:def 3 :
VLabelSelector = 7;

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

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

existence
ex b₁ being GraphStruct st
( b₁ is [Graph-like] & b₁ is [Weighted] & b₁ is [ELabeled] & b₁ is [VLabeled] )

proof end;

end;

definition

mode WGraph is [Weighted] _Graph;
mode EGraph is [ELabeled] _Graph;
mode VGraph is [VLabeled] _Graph;
mode WEGraph is [Weighted] [ELabeled] _Graph;
mode WVGraph is [Weighted] [VLabeled] _Graph;
mode EVGraph is [ELabeled] [VLabeled] _Graph;
mode WEVGraph is [Weighted] [ELabeled] [VLabeled] _Graph;

end;

definition

let G be WGraph;

func the_Weight_of G -> ManySortedSet of the_Edges_of G equals :: GLIB_003:def 7
G . WeightSelector;

coherence
G . WeightSelector is ManySortedSet of the_Edges_of G 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;

func the_ELabel_of G -> Function equals :: GLIB_003:def 8
G . ELabelSelector;

coherence
G . ELabelSelector is Function

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;

func the_VLabel_of G -> Function equals :: GLIB_003:def 9
G . VLabelSelector;

coherence
G . VLabelSelector is Function

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 (the_ELabel_of G) c= the_Edges_of G

proof end;

Lm2: for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G

proof end;

registration

let G be _Graph;
let X be set ;

cluster G .set (WeightSelector,X) -> [Graph-like] ;

coherence
G .set (WeightSelector,X) is [Graph-like]

proof end;

cluster G .set (ELabelSelector,X) -> [Graph-like] ;

coherence
G .set (ELabelSelector,X) is [Graph-like]

proof end;

cluster G .set (VLabelSelector,X) -> [Graph-like] ;

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 ;

cluster G .set (WeightSelector,X) -> loopless ;

coherence
G .set (WeightSelector,X) is loopless

proof end;

cluster G .set (ELabelSelector,X) -> loopless ;

coherence
G .set (ELabelSelector,X) is loopless

proof end;

cluster G .set (VLabelSelector,X) -> loopless ;

coherence
G .set (VLabelSelector,X) is loopless

proof end;

end;

registration

let G be _trivial _Graph;
let X be set ;

cluster G .set (WeightSelector,X) -> _trivial ;

coherence
G .set (WeightSelector,X) is _trivial

proof end;

cluster G .set (ELabelSelector,X) -> _trivial ;

coherence
G .set (ELabelSelector,X) is _trivial

proof end;

cluster G .set (VLabelSelector,X) -> _trivial ;

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 ;

cluster G .set (WeightSelector,X) -> non-multi ;

coherence
G .set (WeightSelector,X) is non-multi

proof end;

cluster G .set (ELabelSelector,X) -> non-multi ;

coherence
G .set (ELabelSelector,X) is non-multi

proof end;

cluster G .set (VLabelSelector,X) -> non-multi ;

coherence
G .set (VLabelSelector,X) is non-multi

proof end;

end;

registration

let G be non-Dmulti _Graph;
let X be set ;

cluster G .set (WeightSelector,X) -> non-Dmulti ;

coherence
G .set (WeightSelector,X) is non-Dmulti

proof end;

cluster G .set (ELabelSelector,X) -> non-Dmulti ;

coherence
G .set (ELabelSelector,X) is non-Dmulti

proof end;

cluster G .set (VLabelSelector,X) -> non-Dmulti ;

coherence
G .set (VLabelSelector,X) is non-Dmulti

proof end;

end;

registration

let G be connected _Graph;
let X be set ;

cluster G .set (WeightSelector,X) -> connected ;

coherence
G .set (WeightSelector,X) is connected

proof end;

cluster G .set (ELabelSelector,X) -> connected ;

coherence
G .set (ELabelSelector,X) is connected

proof end;

cluster G .set (VLabelSelector,X) -> connected ;

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 ;

cluster G .set (ELabelSelector,X) -> [Weighted] ;

coherence
G .set (ELabelSelector,X) is [Weighted]

proof end;

cluster G .set (VLabelSelector,X) -> [Weighted] ;

coherence
G .set (VLabelSelector,X) is [Weighted]

proof end;

end;

registration

let G be _Graph;
let X be ManySortedSet of the_Edges_of G;

cluster G .set (WeightSelector,X) -> [Weighted] ;

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 (the_Edges_of G),WL;

cluster G .set (WeightSelector,W) -> [Weighted] ;

coherence
G .set (WeightSelector,W) is [Weighted] ;

end;

registration

let G be EGraph;
let X be set ;

cluster G .set (WeightSelector,X) -> [ELabeled] ;

coherence
G .set (WeightSelector,X) is [ELabeled]

proof end;

cluster G .set (VLabelSelector,X) -> [ELabeled] ;

coherence
G .set (VLabelSelector,X) is [ELabeled]

proof end;

end;

registration

let G be _Graph;
let Y be set ;
let X be PartFunc of (the_Edges_of G),Y;

cluster G .set (ELabelSelector,X) -> [ELabeled] ;

coherence
G .set (ELabelSelector,X) is [ELabeled]

proof end;

end;

registration

let G be _Graph;
let X be ManySortedSet of the_Edges_of G;

cluster G .set (ELabelSelector,X) -> [ELabeled] ;

coherence
G .set (ELabelSelector,X) is [ELabeled]

proof end;

end;

registration

let G be VGraph;
let X be set ;

cluster G .set (WeightSelector,X) -> [VLabeled] ;

coherence
G .set (WeightSelector,X) is [VLabeled]

proof end;

cluster G .set (ELabelSelector,X) -> [VLabeled] ;

coherence
G .set (ELabelSelector,X) is [VLabeled]

proof end;

end;

registration

let G be _Graph;
let Y be set ;
let X be PartFunc of (the_Vertices_of G),Y;

cluster G .set (VLabelSelector,X) -> [VLabeled] ;

coherence
G .set (VLabelSelector,X) is [VLabeled]

proof end;

end;

registration

let G be _Graph;
let X be ManySortedSet of the_Vertices_of G;

cluster G .set (VLabelSelector,X) -> [VLabeled] ;

coherence
G .set (VLabelSelector,X) is [VLabeled]

proof end;

end;

registration

let G be _Graph;

cluster G .set (ELabelSelector,{}) -> [ELabeled] ;

coherence
G .set (ELabelSelector,{}) is [ELabeled]

proof end;

cluster G .set (VLabelSelector,{}) -> [VLabeled] ;

coherence
G .set (VLabelSelector,{}) is [VLabeled]

proof end;

end;

registration

let G be _Graph;

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

existence
ex b₁ being Subgraph of G st
( b₁ is [Weighted] & b₁ is [ELabeled] & b₁ 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 = (the_Weight_of G) | (the_Edges_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 = (the_Weight_of G) | (the_Edges_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 = (the_ELabel_of G) | (the_Edges_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 = (the_ELabel_of G) | (the_Edges_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 = (the_VLabel_of G) | (the_Vertices_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 = (the_VLabel_of G) | (the_Vertices_of G2) );

registration

let G be WGraph;

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

existence
ex b₁ being [Weighted] Subgraph of G st b₁ is weight-inheriting

proof end;

end;

registration

let G be EGraph;

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

existence
ex b₁ being [ELabeled] Subgraph of G st b₁ is elabel-inheriting

proof end;

end;

registration

let G be VGraph;

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

existence
ex b₁ being [VLabeled] Subgraph of G st b₁ is vlabel-inheriting

proof end;

end;

registration

let G be WEGraph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] weight-inheriting elabel-inheriting for Subgraph of G;

existence
ex b₁ being [Weighted] [ELabeled] Subgraph of G st
( b₁ is weight-inheriting & b₁ is elabel-inheriting )

proof end;

end;

registration

let G be WVGraph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [VLabeled] weight-inheriting vlabel-inheriting for Subgraph of G;

existence
ex b₁ being [Weighted] [VLabeled] Subgraph of G st
( b₁ is weight-inheriting & b₁ is vlabel-inheriting )

proof end;

end;

registration

let G be EVGraph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting for Subgraph of G;

existence
ex b₁ being [ELabeled] [VLabeled] Subgraph of G st
( b₁ is elabel-inheriting & b₁ is vlabel-inheriting )

proof end;

end;

registration

let G be WEVGraph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting for Subgraph of G;

existence
ex b₁ being [Weighted] [ELabeled] [VLabeled] Subgraph of G st
( b₁ is weight-inheriting & b₁ is elabel-inheriting & b₁ is vlabel-inheriting )

proof end;

end;

definition

let G be WGraph;
mode WSubgraph of G is [Weighted] weight-inheriting Subgraph of G;

end;

definition

let G be EGraph;
mode ESubgraph of G is [ELabeled] elabel-inheriting Subgraph of G;

end;

definition

let G be VGraph;
mode VSubgraph of G is [VLabeled] vlabel-inheriting Subgraph of G;

end;

definition

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

end;

definition

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

end;

definition

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

end;

definition

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

end;

registration

let G be _Graph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for inducedSubgraph of G,V,E;

existence
ex b₁ being inducedSubgraph of G,V,E st
( b₁ is [Weighted] & b₁ is [ELabeled] & b₁ is [VLabeled] )

proof end;

end;

registration

let G be WGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] weight-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [Weighted] inducedSubgraph of G,V,E st b₁ is weight-inheriting

proof end;

end;

registration

let G be EGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [ELabeled] inducedSubgraph of G,V,E st b₁ is elabel-inheriting

proof end;

end;

registration

let G be VGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [VLabeled] inducedSubgraph of G,V,E st b₁ is vlabel-inheriting

proof end;

end;

registration

let G be WEGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] weight-inheriting elabel-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [Weighted] [ELabeled] inducedSubgraph of G,V,E st
( b₁ is weight-inheriting & b₁ is elabel-inheriting )

proof end;

end;

registration

let G be WVGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [VLabeled] weight-inheriting vlabel-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [Weighted] [VLabeled] inducedSubgraph of G,V,E st
( b₁ is weight-inheriting & b₁ is vlabel-inheriting )

proof end;

end;

registration

let G be EVGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b₁ is elabel-inheriting & b₁ is vlabel-inheriting )

proof end;

end;

registration

let G be WEVGraph;
let V, E be set ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting for inducedSubgraph of G,V,E;

existence
ex b₁ being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st
( b₁ is weight-inheriting & b₁ is elabel-inheriting & b₁ 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

let G be WEGraph;
let V, E be set ;
mode inducedWESubgraph of G,V,E is [Weighted] [ELabeled] weight-inheriting elabel-inheriting inducedSubgraph of G,V,E;

end;

definition

let G be WVGraph;
let V, E be set ;
mode inducedWVSubgraph of G,V,E is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting inducedSubgraph of G,V,E;

end;

definition

let G be EVGraph;
let V, E be set ;
mode inducedEVSubgraph of G,V,E is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting inducedSubgraph of G,V,E;

end;

definition

let G be WEVGraph;
let V, E be set ;
mode inducedWEVSubgraph of G,V,E is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting inducedSubgraph of G,V,E;

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 (the_Weight_of G) c= Real>=0 ;

end;

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

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] nonnegative-weighted -> real-weighted for set ;

coherence
for b₁ being WGraph st b₁ is nonnegative-weighted holds
b₁ is real-weighted by XBOOLE_1:1, VALUED_0:def 3;

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

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] real-WEV -> real-weighted real-elabeled real-vlabeled for set ;

coherence
for b₁ being WEVGraph st b₁ is real-WEV holds
( b₁ is real-weighted & b₁ is real-elabeled & b₁ is real-vlabeled ) ;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] real-weighted real-elabeled real-vlabeled -> real-WEV for set ;

coherence
for b₁ being WEVGraph st b₁ is real-weighted & b₁ is real-elabeled & b₁ is real-vlabeled holds
b₁ is real-WEV ;

end;

registration

let G be _Graph;
let X be Function of (the_Edges_of G),REAL;

cluster G .set (WeightSelector,X) -> real-weighted ;

coherence
G .set (WeightSelector,X) is real-weighted by GLIB_000:8;

end;

registration

let G be _Graph;
let X be PartFunc of (the_Edges_of G),REAL;

cluster G .set (ELabelSelector,X) -> real-elabeled ;

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;

cluster G .set (ELabelSelector,X) -> real-elabeled ;

coherence
G .set (ELabelSelector,X) is real-elabeled by GLIB_000:8;

end;

registration

let G be _Graph;
let X be PartFunc of (the_Vertices_of G),REAL;

cluster G .set (VLabelSelector,X) -> real-vlabeled ;

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;

cluster G .set (VLabelSelector,X) -> real-vlabeled ;

coherence
G .set (VLabelSelector,X) is real-vlabeled by GLIB_000:8;

end;

registration

let G be _Graph;

cluster G .set (ELabelSelector,{}) -> real-elabeled ;

coherence
G .set (ELabelSelector,{}) is real-elabeled

proof end;

cluster G .set (VLabelSelector,{}) -> real-vlabeled ;

coherence
G .set (VLabelSelector,{}) is real-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)) -> [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

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite _trivial Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ;

existence
ex b₁ being WEVGraph st
( b₁ is _finite & b₁ is _trivial & b₁ is Tree-like & b₁ is nonnegative-weighted & b₁ is real-WEV )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite non _trivial Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ;

existence
ex b₁ being WEVGraph st
( b₁ is _finite & not b₁ is _trivial & b₁ is Tree-like & b₁ is nonnegative-weighted & b₁ is real-WEV )

proof end;

end;

registration

let G be _finite WGraph;

cluster the_Weight_of G -> finite ;

coherence
the_Weight_of G is finite

proof end;

end;

registration

let G be _finite EGraph;

cluster the_ELabel_of G -> finite ;

coherence
the_ELabel_of G is finite

proof end;

end;

registration

let G be _finite VGraph;

cluster the_VLabel_of G -> finite ;

coherence
the_VLabel_of G is finite

proof end;

end;

registration

let G be real-weighted WGraph;

cluster the_Weight_of G -> real-valued ;

coherence
the_Weight_of G is real-valued by Def13;

end;

registration

let G be real-elabeled EGraph;

cluster the_ELabel_of G -> real-valued ;

coherence
the_ELabel_of G is real-valued by Def15;

end;

registration

let G be real-vlabeled VGraph;

cluster the_VLabel_of G -> real-valued ;

coherence
the_VLabel_of G is real-valued by Def16;

end;

registration

let G be real-weighted WGraph;
let X be set ;

cluster G .set (ELabelSelector,X) -> real-weighted ;

coherence
G .set (ELabelSelector,X) is real-weighted

proof end;

cluster G .set (VLabelSelector,X) -> real-weighted ;

coherence
G .set (VLabelSelector,X) is real-weighted

proof end;

end;

registration

let G be nonnegative-weighted WGraph;
let X be set ;

cluster G .set (ELabelSelector,X) -> nonnegative-weighted ;

coherence
G .set (ELabelSelector,X) is nonnegative-weighted

proof end;

cluster G .set (VLabelSelector,X) -> nonnegative-weighted ;

coherence
G .set (VLabelSelector,X) is nonnegative-weighted

proof end;

end;

registration

let G be real-elabeled EGraph;
let X be set ;

cluster G .set (WeightSelector,X) -> real-elabeled ;

coherence
G .set (WeightSelector,X) is real-elabeled

proof end;

cluster G .set (VLabelSelector,X) -> real-elabeled ;

coherence
G .set (VLabelSelector,X) is real-elabeled

proof end;

end;

registration

let G be real-vlabeled VGraph;
let X be set ;

cluster G .set (WeightSelector,X) -> real-vlabeled ;

coherence
G .set (WeightSelector,X) is real-vlabeled

proof end;

cluster G .set (ELabelSelector,X) -> real-vlabeled ;

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 (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len it holds
it . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) );

existence
ex b₁ being FinSequence st
( len b₁ = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b₁ holds
b₁ . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b₁ holds
b₁ . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) & len b₂ = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b₂ holds
b₂ . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) holds
b₁ = b₂

proof end;

end;

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

definition

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

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 (W .weightSeq());

coherence
Sum (W .weightSeq()) 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 (W .weightSeq());

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 (the_Edges_of G) equals :: GLIB_003:def 20
dom (the_ELabel_of G);

coherence
dom (the_ELabel_of G) is Subset of (the_Edges_of G) by Lm1;

end;

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

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,((the_ELabel_of G) +* (e .--> x))) if e in the_Edges_of G
otherwise G;

coherence
( ( e in the_Edges_of G implies G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph ) & ( not e in the_Edges_of G implies G is EGraph ) )

proof end;

consistency
for b₁ 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,((the_ELabel_of G) +* (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 ;

cluster G .labelEdge (e,x) -> nonnegative-weighted ;

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,((the_VLabel_of G) +* (v .--> x))) if v in the_Vertices_of G
otherwise G;

coherence
( ( v in the_Vertices_of G implies G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph ) & ( not v in the_Vertices_of G implies G is VGraph ) )

proof end;

consistency
for b₁ 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,((the_VLabel_of G) +* (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 (the_Vertices_of G) equals :: GLIB_003:def 23
dom (the_VLabel_of G);

coherence
dom (the_VLabel_of G) is Subset of (the_Vertices_of G) by Lm2;

end;

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

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 ;

cluster G .labelVertex (v,x) -> nonnegative-weighted ;

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;

cluster [Weighted] weight-inheriting -> real-weighted for Subgraph of G;

coherence
for b₁ being WSubgraph of G holds b₁ is real-weighted

proof end;

end;

registration

let G be nonnegative-weighted WGraph;

cluster [Weighted] weight-inheriting -> nonnegative-weighted for Subgraph of G;

coherence
for b₁ being WSubgraph of G holds b₁ is nonnegative-weighted

proof end;

end;

registration

let G be real-elabeled EGraph;

cluster [ELabeled] elabel-inheriting -> real-elabeled for Subgraph of G;

coherence
for b₁ being ESubgraph of G holds b₁ is real-elabeled

proof end;

end;

registration

let G be real-vlabeled VGraph;

cluster [VLabeled] vlabel-inheriting -> real-vlabeled for Subgraph of G;

coherence
for b₁ being VSubgraph of G holds b₁ 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

cluster non empty Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] for set ;

existence
ex b₁ being GraphSeq st
( b₁ is [Weighted] & b₁ is [ELabeled] & b₁ is [VLabeled] )

proof end;

end;

definition

mode WGraphSeq is [Weighted] GraphSeq;
mode EGraphSeq is [ELabeled] GraphSeq;
mode VGraphSeq is [VLabeled] GraphSeq;
mode WEGraphSeq is [Weighted] [ELabeled] GraphSeq;
mode WVGraphSeq is [Weighted] [VLabeled] GraphSeq;
mode EVGraphSeq is [ELabeled] [VLabeled] GraphSeq;
mode WEVGraphSeq is [Weighted] [ELabeled] [VLabeled] GraphSeq;

end;

registration

let GSq be WGraphSeq;
let x be Nat;

cluster GSq . x -> [Weighted] for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is [Weighted] by Def24;

end;

registration

let GSq be EGraphSeq;
let x be Nat;

cluster GSq . x -> [ELabeled] for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ is [ELabeled] by Def25;

end;

registration

let GSq be VGraphSeq;
let x be Nat;

cluster GSq . x -> [VLabeled] for _Graph;

coherence
for b₁ being _Graph st b₁ = GSq . x holds
b₁ 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

cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] real-WEV -> real-weighted real-elabeled real-vlabeled for set ;

coherence
for b₁ being WEVGraphSeq st b₁ is real-WEV holds
( b₁ is real-weighted & b₁ is real-elabeled & b₁ is real-vlabeled )

proof end;

cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] real-weighted real-elabeled real-vlabeled -> real-WEV for set ;

coherence
for b₁ being WEVGraphSeq st b₁ is real-weighted & b₁ is real-elabeled & b₁ is real-vlabeled holds
b₁ is real-WEV

proof end;

end;

registration

cluster non empty Relation-like NAT -defined Function-like total Graph-yielding halting _finite loopless _trivial non-multi simple Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ;

existence
ex b₁ being WEVGraphSeq st
( b₁ is halting & b₁ is _finite & b₁ is loopless & b₁ is _trivial & b₁ is non-multi & b₁ is simple & b₁ is real-WEV & b₁ is nonnegative-weighted & b₁ 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 b₁ being WGraph st b₁ = GSq . x holds
b₁ 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 b₁ being WGraph st b₁ = GSq . x holds
b₁ 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 b₁ being EGraph st b₁ = GSq . x holds
b₁ 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 b₁ being VGraph st b₁ = GSq . x holds
b₁ 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 (the_ELabel_of G) c= the_Edges_of G by Lm1;

theorem :: GLIB_003:6

for G being VGraph holds dom (the_VLabel_of G) 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
(the_Weight_of G2) . x = (the_Weight_of G1) . 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 .weightSeq()) = 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() = <*((the_Weight_of G) . e)*>

proof end;

theorem Th15: :: GLIB_003:15

for G being WGraph
for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq())

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() = (W1 .weightSeq()) ^ (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 (W .last()) .edgesInOut() holds
(W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . 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 (W1 .weightSeq()) 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 Th12, RVSUM_1:72;

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() = (the_Weight_of G) . e

proof end;

theorem :: GLIB_003:23

for G being real-weighted WGraph
for W being Walk of G holds W .cost() = (W .reverse()) .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 (W .last()) .edgesInOut() holds
(W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . 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 (W .weightSeq()) holds
0 <= (W .weightSeq()) . 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 <= (the_Weight_of G) . 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)) = (the_ELabel_of G) +* (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 = (the_ELabel_of G) . 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)) = (the_VLabel_of G) +* (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 = (the_VLabel_of G) . 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() = (G .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 (G .labeledE())) + 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() = (G .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 (G .labeledV())) + 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;