:: GLIB_003 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

registration
let F be real-yielding Relation;
let X be set ;
cluster F | X -> real-yielding ;
coherence
F | X is real-yielding ;
end;

theorem :: GLIB_003:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fs being FinSequence of REAL
for fss being FinSubsequence of fs st ( for i being Nat st i in dom fs holds
0 <= fs . i ) holds
Sum (Seq fss) <= Sum fs
proof end;

definition
func WeightSelector -> Nat equals :: GLIB_003:def 1
5;
coherence
5 is Nat ;
func ELabelSelector -> Nat equals :: GLIB_003:def 2
6;
coherence
6 is Nat ;
func VLabelSelector -> Nat equals :: GLIB_003:def 3
7;
coherence
7 is 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 [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct ;
existence
ex b1 being GraphStruct st
( b1 is [Graph-like] & b1 is [Weighted] & b1 is [ELabeled] & b1 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 -> [Graph-like] finite ;
coherence
G .set WeightSelector ,X is finite
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] finite ;
coherence
G .set ELabelSelector ,X is finite
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] loopless ;
coherence
G .set WeightSelector ,X is loopless
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] loopless ;
coherence
G .set ELabelSelector ,X is loopless
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] trivial ;
coherence
G .set WeightSelector ,X is trivial
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] trivial ;
coherence
G .set ELabelSelector ,X is trivial
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] non trivial ;
coherence
not G .set WeightSelector ,X is trivial
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] non trivial ;
coherence
not G .set ELabelSelector ,X is trivial
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] non-multi ;
coherence
G .set WeightSelector ,X is non-multi
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] non-multi ;
coherence
G .set ELabelSelector ,X is non-multi
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] non-Dmulti ;
coherence
G .set WeightSelector ,X is non-Dmulti
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] non-Dmulti ;
coherence
G .set ELabelSelector ,X is non-Dmulti
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] connected ;
coherence
G .set WeightSelector ,X is connected
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] connected ;
coherence
G .set ELabelSelector ,X is connected
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] 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 -> [Graph-like] loopless non-multi acyclic ;
coherence
G .set WeightSelector ,X is acyclic
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] loopless non-multi acyclic ;
coherence
G .set ELabelSelector ,X is acyclic
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] loopless non-multi 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 -> [Graph-like] [Weighted] ;
coherence
G .set ELabelSelector ,X is [Weighted]
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] [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 -> [Graph-like] [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 -> [Graph-like] [Weighted] ;
coherence
G .set WeightSelector ,W is [Weighted]
proof end;
end;

registration
let G be EGraph;
let X be set ;
cluster G .set WeightSelector ,X -> [Graph-like] [ELabeled] ;
coherence
G .set WeightSelector ,X is [ELabeled]
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] [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 -> [Graph-like] [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 -> [Graph-like] [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 -> [Graph-like] [VLabeled] ;
coherence
G .set WeightSelector ,X is [VLabeled]
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] [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 -> [Graph-like] [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 -> [Graph-like] [VLabeled] ;
coherence
G .set VLabelSelector ,X is [VLabeled]
proof end;
end;

registration
let G be _Graph;
cluster G .set ELabelSelector ,{} -> [Graph-like] [ELabeled] ;
coherence
G .set ELabelSelector ,{} is [ELabeled]
proof end;
cluster G .set VLabelSelector ,{} -> [Graph-like] [VLabeled] ;
coherence
G .set VLabelSelector ,{} is [VLabeled]
proof end;
end;

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

definition
let G be WGraph;
let G2 be [Weighted] Subgraph of G;
attr G2 is weight-inheriting means :Def10: :: GLIB_003:def 10
 the_Weight_of G2 = (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 [Weighted] weight-inheriting Subgraph of G;
existence
ex b1 being [Weighted] Subgraph of G st b1 is weight-inheriting
proof end;
end;

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

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

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

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

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

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

definition
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 [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E;
existence
ex b1 being inducedSubgraph of G,V,E st
( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] )
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

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 nonnegative-weighted -> real-weighted GraphStruct ;
coherence
for b1 being WGraph st b1 is nonnegative-weighted holds
b1 is real-weighted
proof end;
end;

definition
let G be EGraph;
attr G is real-elabeled means :Def15: :: GLIB_003:def 15
 the_ELabel_of G is real-yielding;
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-yielding );

definition
let G be VGraph;
attr G is real-vlabeled means :Def16: :: GLIB_003:def 16
 the_VLabel_of G is real-yielding;
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-yielding );

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

:: deftheorem Def17 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 real-WEV -> real-weighted real-elabeled real-vlabeled GraphStruct ;
coherence
for b1 being WEVGraph st b1 is real-WEV holds
( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled ) by Def17;
cluster real-weighted real-elabeled real-vlabeled -> real-WEV GraphStruct ;
coherence
for b1 being WEVGraph st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds
b1 is real-WEV by Def17;
end;

registration
let G be _Graph;
let X be Function of the_Edges_of G, REAL ;
cluster G .set WeightSelector ,X -> [Graph-like] [Weighted] real-weighted ;
coherence
G .set WeightSelector ,X is real-weighted
proof end;
end;

registration
let G be _Graph;
let X be PartFunc of the_Edges_of G, REAL ;
cluster G .set ELabelSelector ,X -> [Graph-like] [ELabeled] real-elabeled ;
coherence
G .set ELabelSelector ,X is real-elabeled
proof end;
end;

registration
let G be _Graph;
let X be real-yielding ManySortedSet of the_Edges_of G;
cluster G .set ELabelSelector ,X -> [Graph-like] [ELabeled] real-elabeled ;
coherence
G .set ELabelSelector ,X is real-elabeled
proof end;
end;

registration
let G be _Graph;
let X be PartFunc of the_Vertices_of G, REAL ;
cluster G .set VLabelSelector ,X -> [Graph-like] [VLabeled] real-vlabeled ;
coherence
G .set VLabelSelector ,X is real-vlabeled
proof end;
end;

registration
let G be _Graph;
let X be real-yielding ManySortedSet of the_Vertices_of G;
cluster G .set VLabelSelector ,X -> [Graph-like] [VLabeled] real-vlabeled ;
coherence
G .set VLabelSelector ,X is real-vlabeled
proof end;
end;

registration
let G be _Graph;
cluster G .set ELabelSelector ,{} -> [Graph-like] [ELabeled] real-elabeled ;
coherence
G .set ELabelSelector ,{} is real-elabeled
proof end;
cluster G .set VLabelSelector ,{} -> [Graph-like] [VLabeled] 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 number ;
cluster G .set VLabelSelector ,(v .--> val) -> [Graph-like] [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 number ;
cluster G .set VLabelSelector ,(v .--> val) -> [Graph-like] [VLabeled] real-vlabeled ;
coherence
G .set VLabelSelector ,(v .--> val) is real-vlabeled
proof end;
end;

registration
cluster finite trivial Tree-like real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV GraphStruct ;
existence
ex b1 being WEVGraph st
( b1 is finite & b1 is trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV )
proof end;
cluster finite non trivial Tree-like real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV GraphStruct ;
existence
ex b1 being WEVGraph st
( b1 is finite & not b1 is trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV )
proof end;
end;

registration
let G be finite WGraph;
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-yielding ;
coherence
the_Weight_of G is real-yielding by Def13;
end;

registration
let G be real-elabeled EGraph;
cluster the_ELabel_of G -> real-yielding ;
coherence
the_ELabel_of G is real-yielding by Def15;
end;

registration
let G be real-vlabeled VGraph;
cluster the_VLabel_of G -> real-yielding ;
coherence
the_VLabel_of G is real-yielding by Def16;
end;

registration
let G be real-weighted WGraph;
let X be set ;
cluster G .set ELabelSelector ,X -> [Graph-like] [Weighted] real-weighted ;
coherence
G .set ELabelSelector ,X is real-weighted
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] [Weighted] 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 -> [Graph-like] [Weighted] real-weighted nonnegative-weighted ;
coherence
G .set ELabelSelector ,X is nonnegative-weighted
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] [Weighted] real-weighted 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 -> [Graph-like] [ELabeled] real-elabeled ;
coherence
G .set WeightSelector ,X is real-elabeled
proof end;
cluster G .set VLabelSelector ,X -> [Graph-like] [ELabeled] 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 -> [Graph-like] [VLabeled] real-vlabeled ;
coherence
G .set WeightSelector ,X is real-vlabeled
proof end;
cluster G .set ELabelSelector ,X -> [Graph-like] [VLabeled] 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 b1 being FinSequence st
( len b1 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) & len b2 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len b2 holds
b2 . n = (the_Weight_of G) . ((W .edgeSeq() ) . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :
for G being WGraph
for W being Walk of G
for b3 being FinSequence holds
( b3 = W .weightSeq() iff ( len b3 = len (W .edgeSeq() ) & ( for n being Nat st 1 <= n & n <= len b3 holds
b3 . 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 set ;
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 b1 being EGraph holds verum ;
end;

:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :
for G being EGraph
for e, x being set 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 -> loopless non-multi 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 -> [Weighted] 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 -> [Weighted] real-weighted 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 -> [VLabeled] real-vlabeled ;
coherence
G .labelEdge e,x is real-vlabeled
proof end;
end;

definition
let G be VGraph;
let v, x be set ;
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 b1 being VGraph holds verum ;
end;

:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :
for G being VGraph
for v, x being set 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 -> loopless non-multi 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 -> [Weighted] 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 -> [Weighted] real-weighted 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 -> [ELabeled] 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 -> real-weighted Subgraph of G;
coherence
for b1 being WSubgraph of G holds b1 is real-weighted
proof end;
end;

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

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

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

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

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

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

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

registration
cluster [Weighted] [ELabeled] [VLabeled] ManySortedSet of NAT ;
existence
ex b1 being GraphSeq st
( b1 is [Weighted] & b1 is [ELabeled] & b1 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] ;
coherence
GSq .-> x is [Weighted] by Def24;
end;

registration
let GSq be EGraphSeq;
let x be Nat;
cluster GSq .-> x -> [ELabeled] ;
coherence
GSq .-> x is [ELabeled] by Def25;
end;

registration
let GSq be VGraphSeq;
let x be Nat;
cluster GSq .-> x -> [VLabeled] ;
coherence
GSq .-> x 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 :Def31: :: GLIB_003:def 31
for x being Nat holds GSq .-> x is real-WEV;
end;

:: deftheorem Def31 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 real-WEV -> real-weighted real-elabeled real-vlabeled ManySortedSet of NAT ;
coherence
for b1 being WEVGraphSeq st b1 is real-WEV holds
( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled )
proof end;
cluster real-weighted real-elabeled real-vlabeled -> real-WEV ManySortedSet of NAT ;
coherence
for b1 being WEVGraphSeq st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds
b1 is real-WEV
proof end;
end;

registration
cluster halting finite loopless trivial non-multi simple Tree-like real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV ManySortedSet of NAT ;
existence
ex b1 being WEVGraphSeq st
( b1 is halting & b1 is finite & b1 is loopless & b1 is trivial & b1 is non-multi & b1 is simple & b1 is real-WEV & b1 is nonnegative-weighted & b1 is Tree-like )
proof end;
end;

registration
let GSq be real-weighted WGraphSeq;
let x be Nat;
cluster GSq .-> x -> [Weighted] real-weighted ;
coherence
GSq .-> x is real-weighted by Def27;
end;

registration
let GSq be nonnegative-weighted WGraphSeq;
let x be Nat;
cluster GSq .-> x -> [Weighted] real-weighted nonnegative-weighted ;
coherence
GSq .-> x is nonnegative-weighted by Def28;
end;

registration
let GSq be real-elabeled EGraphSeq;
let x be Nat;
cluster GSq .-> x -> [ELabeled] real-elabeled ;
coherence
GSq .-> x is real-elabeled by Def29;
end;

registration
let GSq be real-vlabeled VGraphSeq;
let x be Nat;
cluster GSq .-> x -> [VLabeled] real-vlabeled ;
coherence
GSq .-> x is real-vlabeled by Def30;
end;

theorem :: GLIB_003:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7 ) ;

theorem :: GLIB_003:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( ( 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GLIB_003:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G by Lm1;

theorem :: GLIB_003:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;

theorem :: GLIB_003:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_003:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being EGraph
for X being set holds the_ELabel_of G = the_ELabel_of (G .set WeightSelector ,X) by GLIB_000:12;

theorem :: GLIB_003:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being VGraph
for X being set holds the_VLabel_of G = the_VLabel_of (G .set WeightSelector ,X) by GLIB_000:12;

theorem :: GLIB_003:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WGraph
for X being set holds the_Weight_of G = the_Weight_of (G .set ELabelSelector ,X) by GLIB_000:12;

theorem :: GLIB_003:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being VGraph
for X being set holds the_VLabel_of G = the_VLabel_of (G .set ELabelSelector ,X) by GLIB_000:12;

theorem :: GLIB_003:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WGraph
for X being set holds the_Weight_of G = the_Weight_of (G .set VLabelSelector ,X) by GLIB_000:12;

theorem :: GLIB_003:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being EGraph
for X being set holds the_ELabel_of G = the_ELabel_of (G .set VLabelSelector ,X) by GLIB_000:12;

theorem :: GLIB_003:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th19: :: GLIB_003:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WGraph
for W being Walk of G st W is trivial holds
W .weightSeq() = {}
proof end;

theorem :: GLIB_003:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WGraph
for W being Walk of G holds len (W .weightSeq() ) = W .length()
proof end;

theorem Th21: :: GLIB_003:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th22: :: GLIB_003:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WGraph
for W being Walk of G holds (W .reverse() ) .weightSeq() = Rev (W .weightSeq() )
proof end;

theorem Th23: :: GLIB_003:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th24: :: GLIB_003:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th25: :: GLIB_003:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being real-weighted WGraph
for W1 being Walk of G
for W2 being Subwalk of W1 ex ws being FinSubsequence of W1 .weightSeq() st W2 .weightSeq() = Seq ws
proof end;

theorem Th26: :: GLIB_003:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th27: :: GLIB_003:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_003:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being real-weighted WGraph
for W being Walk of G st W is trivial holds
W .cost() = 0 by RVSUM_1:102, Th19;

theorem :: GLIB_003:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being real-weighted WGraph
for W being Walk of G holds W .cost() = (W .reverse() ) .cost()
proof end;

theorem :: GLIB_003:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th26;

theorem :: GLIB_003:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th27;

theorem Th35: :: GLIB_003:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being nonnegative-weighted WGraph
for W being Walk of G
for n being Nat st n in dom (W .weightSeq() ) holds
0 <= (W .weightSeq() ) . n
proof end;

theorem :: GLIB_003:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being nonnegative-weighted WGraph
for W being Walk of G holds 0 <= W .cost()
proof end;

theorem :: GLIB_003:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th39: :: GLIB_003:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being EGraph
for e, x being set holds G == G .labelEdge e,x
proof end;

theorem :: GLIB_003:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WEGraph
for e, x being set holds the_Weight_of G = the_Weight_of (G .labelEdge e,x)
proof end;

theorem Th43: :: GLIB_003:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th45: :: GLIB_003:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being VGraph
for v, x being set holds G == G .labelVertex v,x
proof end;

theorem :: GLIB_003:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being WVGraph
for v, x being set holds the_Weight_of G = the_Weight_of (G .labelVertex v,x)
proof end;

theorem Th49: :: GLIB_003:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_003:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being EGraph st the_ELabel_of G1 = the_ELabel_of G2 holds
G1 .labeledE() = G2 .labeledE() ;

theorem Th52: :: GLIB_003:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being EVGraph
for v, x being set holds G .labeledE() = (G .labelVertex v,x) .labeledE() by Th49;

theorem :: GLIB_003:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_003:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being VGraph st the_VLabel_of G1 = the_VLabel_of G2 holds
G1 .labeledV() = G2 .labeledV() ;

theorem Th59: :: GLIB_003:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being EVGraph
for e, x being set holds G .labeledV() = (G .labelEdge e,x) .labeledV() by Th43;

theorem :: GLIB_003:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being VGraph
for v being Vertex of G
for x being set holds v in (G .labelVertex v,x) .labeledV()
proof end;