:: by Gilbert Lee

::

:: Received February 22, 2005

:: Copyright (c) 2005-2017 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;

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

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 )

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

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

definition

let G be GraphStruct;

end;
attr G is [Weighted] means :Def4: :: GLIB_003:def 4

( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G );

( 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 ) );

( 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 ) );

( VLabelSelector in dom G & ex f being Function st

( G . VLabelSelector = f & dom f c= the_Vertices_of G ) );

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

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 ) ) );

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 ) ) );

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

ex b_{1} being GraphStruct st

( b_{1} is [Graph-like] & b_{1} is [Weighted] & b_{1} is [ELabeled] & b_{1} is [VLabeled] )
end;

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

existence ex b

( b

proof 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;
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;

definition
end;

:: deftheorem defines the_Weight_of GLIB_003:def 7 :

for G being WGraph holds the_Weight_of G = G . WeightSelector;

for G being WGraph holds the_Weight_of G = G . WeightSelector;

:: deftheorem defines the_ELabel_of GLIB_003:def 8 :

for G being EGraph holds the_ELabel_of G = G . ELabelSelector;

for G being EGraph holds the_ELabel_of G = G . ELabelSelector;

:: deftheorem defines the_VLabel_of GLIB_003:def 9 :

for G being VGraph holds the_VLabel_of G = G . VLabelSelector;

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 ;

coherence

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

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

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

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

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 ;

coherence

G .set (WeightSelector,X) is finite

G .set (ELabelSelector,X) is finite

G .set (VLabelSelector,X) is finite

end;
let X be set ;

coherence

G .set (WeightSelector,X) is finite

proof end;

coherence G .set (ELabelSelector,X) is finite

proof end;

coherence G .set (VLabelSelector,X) is finite

proof end;

registration

let G be loopless _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is loopless

G .set (ELabelSelector,X) is loopless

G .set (VLabelSelector,X) is loopless

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

registration

let G be trivial _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is trivial

G .set (ELabelSelector,X) is trivial

G .set (VLabelSelector,X) is trivial

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

registration

let G be non trivial _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is trivial

not G .set (ELabelSelector,X) is trivial

not G .set (VLabelSelector,X) is trivial

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is trivial

proof end;

coherence not G .set (ELabelSelector,X) is trivial

proof end;

coherence not G .set (VLabelSelector,X) is trivial

proof end;

registration

let G be non-multi _Graph;

let X be set ;

coherence

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

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

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

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

registration

let G be non-Dmulti _Graph;

let X be set ;

coherence

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

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

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

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

registration

let G be connected _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is connected

G .set (ELabelSelector,X) is connected

G .set (VLabelSelector,X) is connected

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

registration

let G be acyclic _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is acyclic

G .set (ELabelSelector,X) is acyclic

G .set (VLabelSelector,X) is acyclic

end;
let X be set ;

coherence

G .set (WeightSelector,X) is acyclic

proof end;

coherence G .set (ELabelSelector,X) is acyclic

proof end;

coherence G .set (VLabelSelector,X) is acyclic

proof end;

registration

let G be WGraph;

let X be set ;

coherence

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

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

end;
let X be set ;

coherence

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

proof end;

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

proof end;

registration

let G be _Graph;

let X be ManySortedSet of the_Edges_of G;

coherence

G .set (WeightSelector,X) is [Weighted]

end;
let X be ManySortedSet of the_Edges_of G;

coherence

G .set (WeightSelector,X) is [Weighted]

proof end;

registration

let G be _Graph;

let WL be non empty set ;

let W be Function of (the_Edges_of G),WL;

coherence

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

end;
let WL be non empty set ;

let W be Function of (the_Edges_of G),WL;

coherence

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

registration

let G be EGraph;

let X be set ;

coherence

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

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

end;
let X be set ;

coherence

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

proof end;

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

proof end;

registration

let G be _Graph;

let Y be set ;

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

coherence

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

end;
let Y be set ;

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

coherence

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

proof end;

registration

let G be _Graph;

let X be ManySortedSet of the_Edges_of G;

coherence

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

end;
let X be ManySortedSet of the_Edges_of G;

coherence

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

proof end;

registration

let G be VGraph;

let X be set ;

coherence

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

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

end;
let X be set ;

coherence

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

proof end;

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

proof end;

registration

let G be _Graph;

let Y be set ;

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

coherence

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

end;
let Y be set ;

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

coherence

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

proof end;

registration

let G be _Graph;

let X be ManySortedSet of the_Vertices_of G;

coherence

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

end;
let X be ManySortedSet of the_Vertices_of G;

coherence

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

proof end;

registration

let G be _Graph;

coherence

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

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

end;
coherence

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

proof end;

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

proof end;

registration

let G be _Graph;

ex b_{1} being Subgraph of G st

( b_{1} is [Weighted] & b_{1} is [ELabeled] & b_{1} is [VLabeled] )

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

existence ex b

( b

proof end;

definition

let G be WGraph;

let G2 be [Weighted] Subgraph of G;

end;
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);

the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2);

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

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;

end;
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);

the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2);

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

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;

end;
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);

the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2);

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

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;

ex b_{1} being [Weighted] Subgraph of G st b_{1} is weight-inheriting

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

existence ex b

proof end;

registration

let G be EGraph;

ex b_{1} being [ELabeled] Subgraph of G st b_{1} is elabel-inheriting

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

existence ex b

proof end;

registration

let G be VGraph;

ex b_{1} being [VLabeled] Subgraph of G st b_{1} is vlabel-inheriting

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

existence ex b

proof end;

registration

let G be WEGraph;

ex b_{1} being [Weighted] [ELabeled] Subgraph of G st

( b_{1} is weight-inheriting & b_{1} is elabel-inheriting )

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

existence ex b

( b

proof end;

registration

let G be WVGraph;

ex b_{1} being [Weighted] [VLabeled] Subgraph of G st

( b_{1} is weight-inheriting & b_{1} is vlabel-inheriting )

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

existence ex b

( b

proof end;

registration

let G be EVGraph;

ex b_{1} being [ELabeled] [VLabeled] Subgraph of G st

( b_{1} is elabel-inheriting & b_{1} is vlabel-inheriting )

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

existence ex b

( b

proof end;

registration

let G be WEVGraph;

ex b_{1} being [Weighted] [ELabeled] [VLabeled] Subgraph of G st

( b_{1} is weight-inheriting & b_{1} is elabel-inheriting & b_{1} is vlabel-inheriting )

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

( b

proof end;

definition

let G be WEGraph;

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

end;
mode WESubgraph of G is [Weighted] [ELabeled] weight-inheriting elabel-inheriting Subgraph of G;

definition

let G be WVGraph;

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

end;
mode WVSubgraph of G is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting Subgraph of G;

definition

let G be EVGraph;

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

end;
mode EVSubgraph of G is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting Subgraph of G;

definition

let G be WEVGraph;

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

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

registration

let G be _Graph;

let V, E be set ;

ex b_{1} being inducedSubgraph of G,V,E st

( b_{1} is [Weighted] & b_{1} is [ELabeled] & b_{1} is [VLabeled] )

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

( b

proof end;

registration

let G be WGraph;

let V, E be set ;

ex b_{1} being [Weighted] inducedSubgraph of G,V,E st b_{1} is weight-inheriting

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

proof end;

registration

let G be EGraph;

let V, E be set ;

ex b_{1} being [ELabeled] inducedSubgraph of G,V,E st b_{1} is elabel-inheriting

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

proof end;

registration

let G be VGraph;

let V, E be set ;

ex b_{1} being [VLabeled] inducedSubgraph of G,V,E st b_{1} is vlabel-inheriting

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

proof end;

registration

let G be WEGraph;

let V, E be set ;

ex b_{1} being [Weighted] [ELabeled] inducedSubgraph of G,V,E st

( b_{1} is weight-inheriting & b_{1} is elabel-inheriting )

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

( b

proof end;

registration

let G be WVGraph;

let V, E be set ;

ex b_{1} being [Weighted] [VLabeled] inducedSubgraph of G,V,E st

( b_{1} is weight-inheriting & b_{1} is vlabel-inheriting )

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

( b

proof end;

registration

let G be EVGraph;

let V, E be set ;

ex b_{1} being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st

( b_{1} is elabel-inheriting & b_{1} is vlabel-inheriting )

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

( b

proof end;

registration

let G be WEVGraph;

let V, E be set ;

ex b_{1} being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st

( b_{1} is weight-inheriting & b_{1} is elabel-inheriting & b_{1} is vlabel-inheriting )

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

( b

proof 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;
let V, E be set ;

mode inducedWSubgraph of G,V,E is [Weighted] weight-inheriting inducedSubgraph of G,V,E;

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;
let V, E be set ;

mode inducedESubgraph of G,V,E is [ELabeled] elabel-inheriting inducedSubgraph of G,V,E;

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;
let V, E be set ;

mode inducedVSubgraph of G,V,E is [VLabeled] vlabel-inheriting inducedSubgraph of G,V,E;

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;
let V, E be set ;

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

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;
let V, E be set ;

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

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;
let V, E be set ;

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

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

definition

let G be WGraph;

let V be set ;

mode inducedWSubgraph of G,V is inducedWSubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedWSubgraph of G,V is inducedWSubgraph of G,V,G .edgesBetween V;

definition

let G be EGraph;

let V be set ;

mode inducedESubgraph of G,V is inducedESubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedESubgraph of G,V is inducedESubgraph of G,V,G .edgesBetween V;

definition

let G be VGraph;

let V be set ;

mode inducedVSubgraph of G,V is inducedVSubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedVSubgraph of G,V is inducedVSubgraph of G,V,G .edgesBetween V;

definition

let G be WEGraph;

let V be set ;

mode inducedWESubgraph of G,V is inducedWESubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedWESubgraph of G,V is inducedWESubgraph of G,V,G .edgesBetween V;

definition

let G be WVGraph;

let V be set ;

mode inducedWVSubgraph of G,V is inducedWVSubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedWVSubgraph of G,V is inducedWVSubgraph of G,V,G .edgesBetween V;

definition

let G be EVGraph;

let V be set ;

mode inducedEVSubgraph of G,V is inducedEVSubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedEVSubgraph of G,V is inducedEVSubgraph of G,V,G .edgesBetween V;

definition

let G be WEVGraph;

let V be set ;

mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G,V,G .edgesBetween V;

end;
let V be set ;

mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G,V,G .edgesBetween V;

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

for G being WGraph holds

( G is real-weighted iff the_Weight_of G is real-valued );

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

for G being WGraph holds

( G is nonnegative-weighted iff rng (the_Weight_of G) c= Real>=0 );

registration

for b_{1} being WGraph st b_{1} is nonnegative-weighted holds

b_{1} is real-weighted
by XBOOLE_1:1, VALUED_0:def 3;

end;

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

coherence for b

b

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

for G being EGraph holds

( G is real-elabeled iff the_ELabel_of G is real-valued );

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

for G being VGraph holds

( G is real-vlabeled iff the_VLabel_of G is real-valued );

definition

let G be WEVGraph;

end;
attr G is real-WEV means :: GLIB_003:def 17

( G is real-weighted & G is real-elabeled & G is real-vlabeled );

( G is real-weighted & G is real-elabeled & G is real-vlabeled );

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

for G being WEVGraph holds

( G is real-WEV iff ( G is real-weighted & G is real-elabeled & G is real-vlabeled ) );

registration

for b_{1} being WEVGraph st b_{1} is real-WEV holds

( b_{1} is real-weighted & b_{1} is real-elabeled & b_{1} is real-vlabeled )
;

for b_{1} being WEVGraph st b_{1} is real-weighted & b_{1} is real-elabeled & b_{1} is real-vlabeled holds

b_{1} is real-WEV
;

end;

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

( b

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

b

registration

let G be _Graph;

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

coherence

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

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

coherence

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

registration

let G be _Graph;

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

coherence

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

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

coherence

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

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;
let X be real-valued ManySortedSet of the_Edges_of G;

coherence

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

registration

let G be _Graph;

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

coherence

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

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

coherence

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

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;
let X be real-valued ManySortedSet of the_Vertices_of G;

coherence

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

registration

let G be _Graph;

coherence

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

G .set (VLabelSelector,{}) is real-vlabeled

end;
coherence

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

proof end;

coherence G .set (VLabelSelector,{}) is real-vlabeled

proof end;

registration

let G be _Graph;

let v be Vertex of G;

let val be Real;

coherence

G .set (VLabelSelector,(v .--> val)) is [VLabeled]

end;
let v be Vertex of G;

let val be Real;

coherence

G .set (VLabelSelector,(v .--> val)) is [VLabeled]

proof end;

registration

let G be _Graph;

let v be Vertex of G;

let val be Real;

coherence

G .set (VLabelSelector,(v .--> val)) is real-vlabeled

end;
let v be Vertex of G;

let val be Real;

coherence

G .set (VLabelSelector,(v .--> val)) is real-vlabeled

proof end;

registration

ex b_{1} being WEVGraph st

( b_{1} is finite & b_{1} is trivial & b_{1} is Tree-like & b_{1} is nonnegative-weighted & b_{1} is real-WEV )

ex b_{1} being WEVGraph st

( b_{1} is finite & not b_{1} is trivial & b_{1} is Tree-like & b_{1} is nonnegative-weighted & b_{1} is real-WEV )
end;

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

( b

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

( b

proof end;

registration

let G be real-weighted WGraph;

let X be set ;

coherence

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

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

end;
let X be set ;

coherence

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

proof end;

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

proof end;

registration

let G be nonnegative-weighted WGraph;

let X be set ;

coherence

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

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

end;
let X be set ;

coherence

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

proof end;

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

proof end;

registration

let G be real-elabeled EGraph;

let X be set ;

coherence

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

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

end;
let X be set ;

coherence

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

proof end;

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

proof end;

registration

let G be real-vlabeled VGraph;

let X be set ;

coherence

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

G .set (ELabelSelector,X) is real-vlabeled

end;
let X be set ;

coherence

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

proof end;

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

proof end;

definition

let G be WGraph;

let W be Walk of G;

ex b_{1} being FinSequence st

( len b_{1} = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) )

for b_{1}, b_{2} being FinSequence st len b_{1} = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) & len b_{2} = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b_{2} holds

b_{2} . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for G being WGraph

for W being Walk of G

for b_{3} being FinSequence holds

( b_{3} = W .weightSeq() iff ( len b_{3} = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b_{3} holds

b_{3} . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) );

for G being WGraph

for W being Walk of G

for b

( b

b

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

end;
let W be Walk of G;

:: original: .weightSeq()

redefine func W .weightSeq() -> FinSequence of REAL ;

coherence

W .weightSeq() is FinSequence of REAL

proof end;

definition
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());

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

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

for G being EGraph holds G .labeledE() = dom (the_ELabel_of G);

for G being EGraph holds G .labeledE() = dom (the_ELabel_of G);

definition

let G be EGraph;

let e, x be object ;

( ( 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 ) )

for b_{1} being EGraph holds verum
;

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

otherwise G;

( ( 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

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

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

registration
end;

registration
end;

registration

let G be non trivial EGraph;

let e, x be set ;

coherence

not G .labelEdge (e,x) is trivial

end;
let e, x be set ;

coherence

not G .labelEdge (e,x) is trivial

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let G be real-weighted WEGraph;

let e, x be set ;

coherence

G .labelEdge (e,x) is real-weighted

end;
let e, x be set ;

coherence

G .labelEdge (e,x) is real-weighted

proof end;

registration

let G be nonnegative-weighted WEGraph;

let e, x be set ;

coherence

G .labelEdge (e,x) is nonnegative-weighted

end;
let e, x be set ;

coherence

G .labelEdge (e,x) is nonnegative-weighted

proof end;

registration

let G be real-elabeled EGraph;

let e be set ;

let x be Real;

coherence

G .labelEdge (e,x) is real-elabeled

end;
let e be set ;

let x be Real;

coherence

G .labelEdge (e,x) is real-elabeled

proof end;

registration

let G be real-vlabeled EVGraph;

let e, x be set ;

coherence

G .labelEdge (e,x) is real-vlabeled

end;
let e, x be set ;

coherence

G .labelEdge (e,x) is real-vlabeled

proof end;

definition

let G be VGraph;

let v, x be object ;

( ( 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 ) )

for b_{1} being VGraph holds verum
;

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

otherwise G;

( ( 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

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

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;

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

end;
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);

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

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

for G being VGraph holds G .labeledV() = dom (the_VLabel_of G);

for G being VGraph holds G .labeledV() = dom (the_VLabel_of G);

registration
end;

registration
end;

registration
end;

registration

let G be non trivial VGraph;

let v, x be set ;

coherence

not G .labelVertex (v,x) is trivial

end;
let v, x be set ;

coherence

not G .labelVertex (v,x) is trivial

proof end;

registration
end;

registration

let G be non-Dmulti VGraph;

let v, x be set ;

coherence

G .labelVertex (v,x) is non-Dmulti

end;
let v, x be set ;

coherence

G .labelVertex (v,x) is non-Dmulti

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let G be real-weighted WVGraph;

let v, x be set ;

coherence

G .labelVertex (v,x) is real-weighted

end;
let v, x be set ;

coherence

G .labelVertex (v,x) is real-weighted

proof end;

registration

let G be nonnegative-weighted WVGraph;

let v, x be set ;

coherence

G .labelVertex (v,x) is nonnegative-weighted

end;
let v, x be set ;

coherence

G .labelVertex (v,x) is nonnegative-weighted

proof end;

registration

let G be real-elabeled EVGraph;

let v, x be set ;

coherence

G .labelVertex (v,x) is real-elabeled

end;
let v, x be set ;

coherence

G .labelVertex (v,x) is real-elabeled

proof end;

registration

let G be real-vlabeled VGraph;

let v be set ;

let x be Real;

coherence

G .labelVertex (v,x) is real-vlabeled

end;
let v be set ;

let x be Real;

coherence

G .labelVertex (v,x) is real-vlabeled

proof end;

registration

let G be real-weighted WGraph;

coherence

for b_{1} being WSubgraph of G holds b_{1} is real-weighted

end;
coherence

for b

proof end;

registration

let G be nonnegative-weighted WGraph;

coherence

for b_{1} being WSubgraph of G holds b_{1} is nonnegative-weighted

end;
coherence

for b

proof end;

registration

let G be real-elabeled EGraph;

coherence

for b_{1} being ESubgraph of G holds b_{1} is real-elabeled

end;
coherence

for b

proof end;

registration

let G be real-vlabeled VGraph;

coherence

for b_{1} being VSubgraph of G holds b_{1} is real-vlabeled

end;
coherence

for b

proof end;

definition

let GSq be GraphSeq;

end;
attr GSq is [Weighted] means :Def24: :: GLIB_003:def 24

for x being Nat holds GSq . x is [Weighted] ;

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] ;

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] ;

for x being Nat holds GSq . x is [VLabeled] ;

:: 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] );

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] );

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] );

for GSq being GraphSeq holds

( GSq is [VLabeled] iff for x being Nat holds GSq . x is [VLabeled] );

registration

ex b_{1} being GraphSeq st

( b_{1} is [Weighted] & b_{1} is [ELabeled] & b_{1} is [VLabeled] )
end;

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

existence ex b

( b

proof 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;
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;

registration

let GSq be WGraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is [Weighted]
by Def24;

end;
let x be Nat;

coherence

for b

b

registration

let GSq be EGraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is [ELabeled]
by Def25;

end;
let x be Nat;

coherence

for b

b

registration

let GSq be VGraphSeq;

let x be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . x holds

b_{1} is [VLabeled]
by Def26;

end;
let x be Nat;

coherence

for b

b

definition

let GSq be WGraphSeq;

end;
attr GSq is real-weighted means :Def27: :: GLIB_003:def 27

for x being Nat holds GSq . x is real-weighted ;

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 ;

for x being Nat holds GSq . x is nonnegative-weighted ;

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

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 );

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;

end;
attr GSq is real-elabeled means :Def29: :: GLIB_003:def 29

for x being Nat holds GSq . x is real-elabeled ;

for x being Nat holds GSq . x is real-elabeled ;

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

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;

end;
attr GSq is real-vlabeled means :Def30: :: GLIB_003:def 30

for x being Nat holds GSq . x is real-vlabeled ;

for x being Nat holds GSq . x is real-vlabeled ;

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

for GSq being VGraphSeq holds

( GSq is real-vlabeled iff for x being Nat holds GSq . x is real-vlabeled );

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

for GSq being WEVGraphSeq holds

( GSq is real-WEV iff for x being Nat holds GSq . x is real-WEV );

registration

for b_{1} being WEVGraphSeq st b_{1} is real-WEV holds

( b_{1} is real-weighted & b_{1} is real-elabeled & b_{1} is real-vlabeled )

for b_{1} being WEVGraphSeq st b_{1} is real-weighted & b_{1} is real-elabeled & b_{1} is real-vlabeled holds

b_{1} is real-WEV
end;

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

( b

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

b

proof end;

registration

ex b_{1} being WEVGraphSeq st

( b_{1} is halting & b_{1} is finite & b_{1} is loopless & b_{1} is trivial & b_{1} is non-multi & b_{1} is simple & b_{1} is real-WEV & b_{1} is nonnegative-weighted & b_{1} is Tree-like )
end;

cluster 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

( b

proof end;

registration

let GSq be real-weighted WGraphSeq;

let x be Nat;

coherence

for b_{1} being WGraph st b_{1} = GSq . x holds

b_{1} is real-weighted
by Def27;

end;
let x be Nat;

coherence

for b

b

registration

let GSq be nonnegative-weighted WGraphSeq;

let x be Nat;

coherence

for b_{1} being WGraph st b_{1} = GSq . x holds

b_{1} is nonnegative-weighted
by Def28;

end;
let x be Nat;

coherence

for b

b

registration

let GSq be real-elabeled EGraphSeq;

let x be Nat;

coherence

for b_{1} being EGraph st b_{1} = GSq . x holds

b_{1} is real-elabeled
by Def29;

end;
let x be Nat;

coherence

for b

b

registration

let GSq be real-vlabeled VGraphSeq;

let x be Nat;

coherence

for b_{1} being VGraph st b_{1} = GSq . x holds

b_{1} is real-vlabeled
by Def30;

end;
let x be Nat;

coherence

for b

b

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 ) ) ;

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

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

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

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

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

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 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)*>

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 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())

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)*>

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

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()

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()

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 trivial holds

W .cost() = 0 by Th12, RVSUM_1:72;

for W being Walk of G st W is trivial 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

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: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())

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)

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;

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

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

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:30

for G being nonnegative-weighted WGraph

for W1 being Walk of G

for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost()

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

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)

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

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

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)

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

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

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() ;

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}

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()

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

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 )

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;

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()

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() ;

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}

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()

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

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 )

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;

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()

for v being Vertex of G

for x being set holds v in (G .labelVertex (v,x)) .labeledV()

proof end;