:: by Gilbert Lee and Piotr Rudnicki

::

:: Received February 22, 2005

:: Copyright (c) 2005-2019 Association of Mizar Users

Lm1: for F being Function

for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}

proof end;

Lm2: for F being Function

for x, y, z being set st z in dom (F +* (x .--> y)) & not z in dom F holds

x = z

proof end;

theorem Th3: :: GLIB_004:3

for A, B being set

for b being Rbag of A

for b1 being Rbag of B

for b2 being Rbag of A \ B st b = b1 +* b2 holds

Sum b = (Sum b1) + (Sum b2)

for b being Rbag of A

for b1 being Rbag of B

for b2 being Rbag of A \ B st b = b1 +* b2 holds

Sum b = (Sum b1) + (Sum b2)

proof end;

theorem Th5: :: GLIB_004:5

for A being set

for b1, b2 being Rbag of A st ( for x being set st x in A holds

b1 . x <= b2 . x ) holds

Sum b1 <= Sum b2

for b1, b2 being Rbag of A st ( for x being set st x in A holds

b1 . x <= b2 . x ) holds

Sum b1 <= Sum b2

proof end;

theorem :: GLIB_004:6

for A being set

for b1, b2 being Rbag of A st ( for x being set st x in A holds

b1 . x = b2 . x ) holds

Sum b1 = Sum b2

for b1, b2 being Rbag of A st ( for x being set st x in A holds

b1 . x = b2 . x ) holds

Sum b1 = Sum b2

proof end;

theorem :: GLIB_004:7

for A1, A2 being set

for b1 being Rbag of A1

for b2 being Rbag of A2 st b1 = b2 holds

Sum b1 = Sum b2

for b1 being Rbag of A1

for b2 being Rbag of A2 st b1 = b2 holds

Sum b1 = Sum b2

proof end;

theorem Th8: :: GLIB_004:8

for X, x being set

for b being Rbag of X

for y being Real st b = (EmptyBag X) +* (x .--> y) holds

Sum b = y

for b being Rbag of X

for y being Real st b = (EmptyBag X) +* (x .--> y) holds

Sum b = y

proof end;

theorem :: GLIB_004:9

for X, x being set

for b1, b2 being Rbag of X

for y being Real st b2 = b1 +* (x .--> y) holds

Sum b2 = ((Sum b1) + y) - (b1 . x)

for b1, b2 being Rbag of X

for y being Real st b2 = b1 +* (x .--> y) holds

Sum b2 = ((Sum b1) + y) - (b1 . x)

proof end;

definition

let G1 be real-weighted WGraph;

let G2 be WSubgraph of G1;

let v be set ;

end;
let G2 be WSubgraph of G1;

let v be set ;

pred G2 is_mincost_DTree_rooted_at v means :: GLIB_004:def 1

( G2 is Tree-like & ( for x being Vertex of G2 ex W2 being DPath of G2 st

( W2 is_Walk_from v,x & ( for W1 being DPath of G1 st W1 is_Walk_from v,x holds

W2 .cost() <= W1 .cost() ) ) ) );

( G2 is Tree-like & ( for x being Vertex of G2 ex W2 being DPath of G2 st

( W2 is_Walk_from v,x & ( for W1 being DPath of G1 st W1 is_Walk_from v,x holds

W2 .cost() <= W1 .cost() ) ) ) );

:: deftheorem defines is_mincost_DTree_rooted_at GLIB_004:def 1 :

for G1 being real-weighted WGraph

for G2 being WSubgraph of G1

for v being set holds

( G2 is_mincost_DTree_rooted_at v iff ( G2 is Tree-like & ( for x being Vertex of G2 ex W2 being DPath of G2 st

( W2 is_Walk_from v,x & ( for W1 being DPath of G1 st W1 is_Walk_from v,x holds

W2 .cost() <= W1 .cost() ) ) ) ) );

for G1 being real-weighted WGraph

for G2 being WSubgraph of G1

for v being set holds

( G2 is_mincost_DTree_rooted_at v iff ( G2 is Tree-like & ( for x being Vertex of G2 ex W2 being DPath of G2 st

( W2 is_Walk_from v,x & ( for W1 being DPath of G1 st W1 is_Walk_from v,x holds

W2 .cost() <= W1 .cost() ) ) ) ) );

definition

let G be real-weighted WGraph;

let W be DPath of G;

let x, y be set ;

end;
let W be DPath of G;

let x, y be set ;

pred W is_mincost_DPath_from x,y means :: GLIB_004:def 2

( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds

W .cost() <= W2 .cost() ) );

( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds

W .cost() <= W2 .cost() ) );

:: deftheorem defines is_mincost_DPath_from GLIB_004:def 2 :

for G being real-weighted WGraph

for W being DPath of G

for x, y being set holds

( W is_mincost_DPath_from x,y iff ( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds

W .cost() <= W2 .cost() ) ) );

for G being real-weighted WGraph

for W being DPath of G

for x, y being set holds

( W is_mincost_DPath_from x,y iff ( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds

W .cost() <= W2 .cost() ) ) );

definition

let G be finite real-weighted WGraph;

let x, y be set ;

( ( ex W being DWalk of G st W is_Walk_from x,y implies ex b_{1} being Real ex W being DPath of G st

( W is_mincost_DPath_from x,y & b_{1} = W .cost() ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ex b_{1} being Real st b_{1} = 0 ) )

for b_{1}, b_{2} being Real holds

( ( ex W being DWalk of G st W is_Walk_from x,y & ex W being DPath of G st

( W is_mincost_DPath_from x,y & b_{1} = W .cost() ) & ex W being DPath of G st

( W is_mincost_DPath_from x,y & b_{2} = W .cost() ) implies b_{1} = b_{2} ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Real holds verum
;

end;
let x, y be set ;

func G .min_DPath_cost (x,y) -> Real means :Def3: :: GLIB_004:def 3

ex W being DPath of G st

( W is_mincost_DPath_from x,y & it = W .cost() ) if ex W being DWalk of G st W is_Walk_from x,y

otherwise it = 0 ;

existence ex W being DPath of G st

( W is_mincost_DPath_from x,y & it = W .cost() ) if ex W being DWalk of G st W is_Walk_from x,y

otherwise it = 0 ;

( ( ex W being DWalk of G st W is_Walk_from x,y implies ex b

( W is_mincost_DPath_from x,y & b

proof end;

uniqueness for b

( ( ex W being DWalk of G st W is_Walk_from x,y & ex W being DPath of G st

( W is_mincost_DPath_from x,y & b

( W is_mincost_DPath_from x,y & b

proof end;

consistency for b

:: deftheorem Def3 defines .min_DPath_cost GLIB_004:def 3 :

for G being finite real-weighted WGraph

for x, y being set

for b_{4} being Real holds

( ( ex W being DWalk of G st W is_Walk_from x,y implies ( b_{4} = G .min_DPath_cost (x,y) iff ex W being DPath of G st

( W is_mincost_DPath_from x,y & b_{4} = W .cost() ) ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ( b_{4} = G .min_DPath_cost (x,y) iff b_{4} = 0 ) ) );

for G being finite real-weighted WGraph

for x, y being set

for b

( ( ex W being DWalk of G st W is_Walk_from x,y implies ( b

( W is_mincost_DPath_from x,y & b

definition

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector} is non empty finite Subset of NAT ;

end;

func WGraphSelectors -> non empty finite Subset of NAT equals :: GLIB_004:def 4

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector};

coherence {VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector};

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector} is non empty finite Subset of NAT ;

:: deftheorem defines WGraphSelectors GLIB_004:def 4 :

WGraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector};

WGraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector};

Lm3: for G being WGraph holds WGraphSelectors c= dom G

proof end;

registration

let G be WGraph;

coherence

( G | WGraphSelectors is [Graph-like] & G | WGraphSelectors is [Weighted] )

end;
coherence

( G | WGraphSelectors is [Graph-like] & G | WGraphSelectors is [Weighted] )

proof end;

Lm4: for G being WGraph holds

( G == G | WGraphSelectors & the_Weight_of G = the_Weight_of (G | WGraphSelectors) )

proof end;

Lm5: for G being WGraph holds dom (G | WGraphSelectors) = WGraphSelectors

proof end;

definition

let G be WGraph;

ex b_{1} being non empty set st

for x being set holds

( x in b_{1} iff ex G2 being WSubgraph of G st

( x = G2 & dom G2 = WGraphSelectors ) )

for b_{1}, b_{2} being non empty set st ( for x being set holds

( x in b_{1} iff ex G2 being WSubgraph of G st

( x = G2 & dom G2 = WGraphSelectors ) ) ) & ( for x being set holds

( x in b_{2} iff ex G2 being WSubgraph of G st

( x = G2 & dom G2 = WGraphSelectors ) ) ) holds

b_{1} = b_{2}

end;
func G .allWSubgraphs() -> non empty set means :Def5: :: GLIB_004:def 5

for x being set holds

( x in it iff ex G2 being WSubgraph of G st

( x = G2 & dom G2 = WGraphSelectors ) );

existence for x being set holds

( x in it iff ex G2 being WSubgraph of G st

( x = G2 & dom G2 = WGraphSelectors ) );

ex b

for x being set holds

( x in b

( x = G2 & dom G2 = WGraphSelectors ) )

proof end;

uniqueness for b

( x in b

( x = G2 & dom G2 = WGraphSelectors ) ) ) & ( for x being set holds

( x in b

( x = G2 & dom G2 = WGraphSelectors ) ) ) holds

b

proof end;

:: deftheorem Def5 defines .allWSubgraphs() GLIB_004:def 5 :

for G being WGraph

for b_{2} being non empty set holds

( b_{2} = G .allWSubgraphs() iff for x being set holds

( x in b_{2} iff ex G2 being WSubgraph of G st

( x = G2 & dom G2 = WGraphSelectors ) ) );

for G being WGraph

for b

( b

( x in b

( x = G2 & dom G2 = WGraphSelectors ) ) );

definition

let G be WGraph;

let X be non empty Subset of (G .allWSubgraphs());

:: original: Element

redefine mode Element of X -> WSubgraph of G;

coherence

for b_{1} being Element of X holds b_{1} is WSubgraph of G

end;
let X be non empty Subset of (G .allWSubgraphs());

:: original: Element

redefine mode Element of X -> WSubgraph of G;

coherence

for b

proof end;

:: deftheorem defines .cost() GLIB_004:def 6 :

for G being finite real-weighted WGraph holds G .cost() = Sum (the_Weight_of G);

for G being finite real-weighted WGraph holds G .cost() = Sum (the_Weight_of G);

theorem Th10: :: GLIB_004:10

for G1 being finite real-weighted WGraph

for e being set

for G2 being [Weighted] weight-inheriting removeEdge of G1,e st e in the_Edges_of G1 holds

G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e)

for e being set

for G2 being [Weighted] weight-inheriting removeEdge of G1,e st e in the_Edges_of G1 holds

G1 .cost() = (G2 .cost()) + ((the_Weight_of G1) . e)

proof end;

theorem Th11: :: GLIB_004:11

for G being finite real-weighted WGraph

for V1 being non empty Subset of (the_Vertices_of G)

for E1 being Subset of (G .edgesBetween V1)

for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

for V1 being non empty Subset of (the_Vertices_of G)

for E1 being Subset of (G .edgesBetween V1)

for G1 being inducedWSubgraph of G,V1,E1

for e being set

for G2 being inducedWSubgraph of G,V1,E1 \/ {e} st not e in E1 & e in G .edgesBetween V1 holds

(G1 .cost()) + ((the_Weight_of G) . e) = G2 .cost()

proof end;

theorem Th12: :: GLIB_004:12

for G being finite nonnegative-weighted WGraph

for W being DPath of G

for x, y being set

for m, n being Element of NAT st W is_mincost_DPath_from x,y holds

W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()

for W being DPath of G

for x, y being set

for m, n being Element of NAT st W is_mincost_DPath_from x,y holds

W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()

proof end;

theorem :: GLIB_004:13

for G being finite real-weighted WGraph

for W1, W2 being DPath of G

for x, y being set st W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y holds

W1 .cost() = W2 .cost()

for W1, W2 being DPath of G

for x, y being set st W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y holds

W1 .cost() = W2 .cost()

proof end;

theorem Th14: :: GLIB_004:14

for G being finite real-weighted WGraph

for W being DPath of G

for x, y being set st W is_mincost_DPath_from x,y holds

G .min_DPath_cost (x,y) = W .cost() by Def3;

for W being DPath of G

for x, y being set st W is_mincost_DPath_from x,y holds

G .min_DPath_cost (x,y) = W .cost() by Def3;

definition

let G be _Graph;

mode DIJK:Labeling of G is Element of [:(PFuncs ((the_Vertices_of G),REAL)),(bool (the_Edges_of G)):];

end;
mode DIJK:Labeling of G is Element of [:(PFuncs ((the_Vertices_of G),REAL)),(bool (the_Edges_of G)):];

definition

let X1, X3 be set ;

let X2 be non empty set ;

let x be Element of [:(PFuncs (X1,X3)),X2:];

:: original: `1

redefine func x `1 -> Element of PFuncs (X1,X3);

coherence

x `1 is Element of PFuncs (X1,X3) by MCART_1:10;

end;
let X2 be non empty set ;

let x be Element of [:(PFuncs (X1,X3)),X2:];

:: original: `1

redefine func x `1 -> Element of PFuncs (X1,X3);

coherence

x `1 is Element of PFuncs (X1,X3) by MCART_1:10;

registration

let G be finite _Graph;

let L be DIJK:Labeling of G;

coherence

for b_{1} being set st b_{1} = L `1 holds

b_{1} is finite

for b_{1} being set st b_{1} = L `2 holds

b_{1} is finite
;

end;
let L be DIJK:Labeling of G;

coherence

for b

b

proof end;

coherence for b

b

definition

let G be real-weighted WGraph;

let L be DIJK:Labeling of G;

ex b_{1} being Subset of (the_Edges_of G) st

for e1 being set holds

( e1 in b_{1} iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e1 being set holds

( e1 in b_{1} iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) & ( for e1 being set holds

( e1 in b_{2} iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) holds

b_{1} = b_{2}

end;
let L be DIJK:Labeling of G;

func DIJK:NextBestEdges L -> Subset of (the_Edges_of G) means :Def7: :: GLIB_004:def 7

for e1 being set holds

( e1 in it iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) );

existence for e1 being set holds

( e1 in it iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) );

ex b

for e1 being set holds

( e1 in b

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) )

proof end;

uniqueness for b

( e1 in b

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) & ( for e1 being set holds

( e1 in b

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) holds

b

proof end;

:: deftheorem Def7 defines DIJK:NextBestEdges GLIB_004:def 7 :

for G being real-weighted WGraph

for L being DIJK:Labeling of G

for b_{3} being Subset of (the_Edges_of G) holds

( b_{3} = DIJK:NextBestEdges L iff for e1 being set holds

( e1 in b_{3} iff ( e1 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G & ( for e2 being set st e2 DSJoins dom (L `1),(the_Vertices_of G) \ (dom (L `1)),G holds

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) );

for G being real-weighted WGraph

for L being DIJK:Labeling of G

for b

( b

( e1 in b

((L `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) );

definition

let G be real-weighted WGraph;

let L be DIJK:Labeling of G;

( ( DIJK:NextBestEdges L = {} implies L is DIJK:Labeling of G ) & ( not DIJK:NextBestEdges L = {} implies [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] is DIJK:Labeling of G ) )

for b_{1} being DIJK:Labeling of G holds verum
;

end;
let L be DIJK:Labeling of G;

func DIJK:Step L -> DIJK:Labeling of G equals :Def8: :: GLIB_004:def 8

L if DIJK:NextBestEdges L = {}

otherwise [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})];

coherence L if DIJK:NextBestEdges L = {}

otherwise [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})];

( ( DIJK:NextBestEdges L = {} implies L is DIJK:Labeling of G ) & ( not DIJK:NextBestEdges L = {} implies [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] is DIJK:Labeling of G ) )

proof end;

consistency for b

:: deftheorem Def8 defines DIJK:Step GLIB_004:def 8 :

for G being real-weighted WGraph

for L being DIJK:Labeling of G holds

( ( DIJK:NextBestEdges L = {} implies DIJK:Step L = L ) & ( not DIJK:NextBestEdges L = {} implies DIJK:Step L = [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] ) );

for G being real-weighted WGraph

for L being DIJK:Labeling of G holds

( ( DIJK:NextBestEdges L = {} implies DIJK:Step L = L ) & ( not DIJK:NextBestEdges L = {} implies DIJK:Step L = [((L `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges L) .--> (((L `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges L)) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges L)))),((L `2) \/ { the Element of DIJK:NextBestEdges L})] ) );

definition

let G be real-weighted WGraph;

let src be Vertex of G;

coherence

[(src .--> 0),{}] is DIJK:Labeling of G

end;
let src be Vertex of G;

coherence

[(src .--> 0),{}] is DIJK:Labeling of G

proof end;

:: deftheorem defines DIJK:Init GLIB_004:def 9 :

for G being real-weighted WGraph

for src being Vertex of G holds DIJK:Init src = [(src .--> 0),{}];

for G being real-weighted WGraph

for src being Vertex of G holds DIJK:Init src = [(src .--> 0),{}];

definition

let G be real-weighted WGraph;

ex b_{1} being ManySortedSet of NAT st

for n being Nat holds b_{1} . n is DIJK:Labeling of G

end;
mode DIJK:LabelingSeq of G -> ManySortedSet of NAT means :Def10: :: GLIB_004:def 10

for n being Nat holds it . n is DIJK:Labeling of G;

existence for n being Nat holds it . n is DIJK:Labeling of G;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def10 defines DIJK:LabelingSeq GLIB_004:def 10 :

for G being real-weighted WGraph

for b_{2} being ManySortedSet of NAT holds

( b_{2} is DIJK:LabelingSeq of G iff for n being Nat holds b_{2} . n is DIJK:Labeling of G );

for G being real-weighted WGraph

for b

( b

definition

let G be real-weighted WGraph;

let S be DIJK:LabelingSeq of G;

let n be Nat;

:: original: .

redefine func S . n -> DIJK:Labeling of G;

coherence

S . n is DIJK:Labeling of G by Def10;

end;
let S be DIJK:LabelingSeq of G;

let n be Nat;

:: original: .

redefine func S . n -> DIJK:Labeling of G;

coherence

S . n is DIJK:Labeling of G by Def10;

definition

let G be real-weighted WGraph;

let src be Vertex of G;

ex b_{1} being DIJK:LabelingSeq of G st

( b_{1} . 0 = DIJK:Init src & ( for n being Nat holds b_{1} . (n + 1) = DIJK:Step (b_{1} . n) ) )

for b_{1}, b_{2} being DIJK:LabelingSeq of G st b_{1} . 0 = DIJK:Init src & ( for n being Nat holds b_{1} . (n + 1) = DIJK:Step (b_{1} . n) ) & b_{2} . 0 = DIJK:Init src & ( for n being Nat holds b_{2} . (n + 1) = DIJK:Step (b_{2} . n) ) holds

b_{1} = b_{2}

end;
let src be Vertex of G;

func DIJK:CompSeq src -> DIJK:LabelingSeq of G means :Def11: :: GLIB_004:def 11

( it . 0 = DIJK:Init src & ( for n being Nat holds it . (n + 1) = DIJK:Step (it . n) ) );

existence ( it . 0 = DIJK:Init src & ( for n being Nat holds it . (n + 1) = DIJK:Step (it . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines DIJK:CompSeq GLIB_004:def 11 :

for G being real-weighted WGraph

for src being Vertex of G

for b_{3} being DIJK:LabelingSeq of G holds

( b_{3} = DIJK:CompSeq src iff ( b_{3} . 0 = DIJK:Init src & ( for n being Nat holds b_{3} . (n + 1) = DIJK:Step (b_{3} . n) ) ) );

for G being real-weighted WGraph

for src being Vertex of G

for b

( b

definition

let G be real-weighted WGraph;

let src be Vertex of G;

(DIJK:CompSeq src) .Result() is DIJK:Labeling of G

end;
let src be Vertex of G;

func DIJK:SSSP (G,src) -> DIJK:Labeling of G equals :: GLIB_004:def 12

(DIJK:CompSeq src) .Result() ;

coherence (DIJK:CompSeq src) .Result() ;

(DIJK:CompSeq src) .Result() is DIJK:Labeling of G

proof end;

:: deftheorem defines DIJK:SSSP GLIB_004:def 12 :

for G being real-weighted WGraph

for src being Vertex of G holds DIJK:SSSP (G,src) = (DIJK:CompSeq src) .Result() ;

for G being real-weighted WGraph

for src being Vertex of G holds DIJK:SSSP (G,src) = (DIJK:CompSeq src) .Result() ;

theorem Th15: :: GLIB_004:15

for G being finite real-weighted WGraph

for L being DIJK:Labeling of G holds

( ( card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) implies DIJK:NextBestEdges L = {} ) & ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) & ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ) )

for L being DIJK:Labeling of G holds

( ( card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) implies DIJK:NextBestEdges L = {} ) & ( DIJK:NextBestEdges L = {} implies card (dom ((DIJK:Step L) `1)) = card (dom (L `1)) ) & ( card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom ((DIJK:Step L) `1)) = (card (dom (L `1))) + 1 ) )

proof end;

theorem Th16: :: GLIB_004:16

for G being real-weighted WGraph

for L being DIJK:Labeling of G holds

( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )

for L being DIJK:Labeling of G holds

( dom (L `1) c= dom ((DIJK:Step L) `1) & L `2 c= (DIJK:Step L) `2 )

proof end;

theorem Th18: :: GLIB_004:18

for G being real-weighted WGraph

for src being Vertex of G

for i, j being Nat st i <= j holds

( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 )

for src being Vertex of G

for i, j being Nat st i <= j holds

( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 )

proof end;

theorem Th19: :: GLIB_004:19

for G being finite real-weighted WGraph

for src being Vertex of G

for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src

for src being Vertex of G

for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src

proof end;

theorem Th20: :: GLIB_004:20

for G being finite real-weighted WGraph

for src being Vertex of G

for n being Nat holds

( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )

for src being Vertex of G

for n being Nat holds

( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )

proof end;

theorem Th21: :: GLIB_004:21

for G being finite real-weighted WGraph

for s being Vertex of G

for n being Nat holds card (dom (((DIJK:CompSeq s) . n) `1)) = min ((n + 1),(card (G .reachableDFrom s)))

for s being Vertex of G

for n being Nat holds card (dom (((DIJK:CompSeq s) . n) `1)) = min ((n + 1),(card (G .reachableDFrom s)))

proof end;

theorem Th22: :: GLIB_004:22

for G being finite real-weighted WGraph

for src being Vertex of G

for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1))

for src being Vertex of G

for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1))

proof end;

theorem Th23: :: GLIB_004:23

for G being finite nonnegative-weighted WGraph

for s being Vertex of G

for n being Nat

for G2 being inducedWSubgraph of G, dom (((DIJK:CompSeq s) . n) `1),((DIJK:CompSeq s) . n) `2 holds

( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in dom (((DIJK:CompSeq s) . n) `1) holds

G .min_DPath_cost (s,v) = (((DIJK:CompSeq s) . n) `1) . v ) )

for s being Vertex of G

for n being Nat

for G2 being inducedWSubgraph of G, dom (((DIJK:CompSeq s) . n) `1),((DIJK:CompSeq s) . n) `2 holds

( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in dom (((DIJK:CompSeq s) . n) `1) holds

G .min_DPath_cost (s,v) = (((DIJK:CompSeq s) . n) `1) . v ) )

proof end;

registration

let G be finite real-weighted WGraph;

let src be Vertex of G;

coherence

DIJK:CompSeq src is halting by Th24;

end;
let src be Vertex of G;

coherence

DIJK:CompSeq src is halting by Th24;

theorem Th25: :: GLIB_004:25

for G being finite real-weighted WGraph

for s being Vertex of G holds ((DIJK:CompSeq s) .Lifespan()) + 1 = card (G .reachableDFrom s)

for s being Vertex of G holds ((DIJK:CompSeq s) .Lifespan()) + 1 = card (G .reachableDFrom s)

proof end;

theorem Th26: :: GLIB_004:26

for G being finite real-weighted WGraph

for s being Vertex of G holds dom ((DIJK:SSSP (G,s)) `1) = G .reachableDFrom s

for s being Vertex of G holds dom ((DIJK:SSSP (G,s)) `1) = G .reachableDFrom s

proof end;

:: Dijkstra's shortest path algorithm

theorem :: GLIB_004:27

for G being finite nonnegative-weighted WGraph

for s being Vertex of G

for G2 being inducedWSubgraph of G, dom ((DIJK:SSSP (G,s)) `1),(DIJK:SSSP (G,s)) `2 holds

( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in G .reachableDFrom s holds

( v in the_Vertices_of G2 & G .min_DPath_cost (s,v) = ((DIJK:SSSP (G,s)) `1) . v ) ) )

for s being Vertex of G

for G2 being inducedWSubgraph of G, dom ((DIJK:SSSP (G,s)) `1),(DIJK:SSSP (G,s)) `2 holds

( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in G .reachableDFrom s holds

( v in the_Vertices_of G2 & G .min_DPath_cost (s,v) = ((DIJK:SSSP (G,s)) `1) . v ) ) )

proof end;

definition

let G be _Graph;

mode PRIM:Labeling of G is Element of [:(bool (the_Vertices_of G)),(bool (the_Edges_of G)):];

end;
mode PRIM:Labeling of G is Element of [:(bool (the_Vertices_of G)),(bool (the_Edges_of G)):];

registration

let G be finite _Graph;

let L be PRIM:Labeling of G;

coherence

for b_{1} being set st b_{1} = L `1 holds

b_{1} is finite
;

coherence

for b_{1} being set st b_{1} = L `2 holds

b_{1} is finite
;

end;
let L be PRIM:Labeling of G;

coherence

for b

b

coherence

for b

b

definition

let G be real-weighted WGraph;

let L be PRIM:Labeling of G;

ex b_{1} being Subset of (the_Edges_of G) st

for e1 being set holds

( e1 in b_{1} iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e1 being set holds

( e1 in b_{1} iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) & ( for e1 being set holds

( e1 in b_{2} iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) holds

b_{1} = b_{2}

end;
let L be PRIM:Labeling of G;

func PRIM:NextBestEdges L -> Subset of (the_Edges_of G) means :Def13: :: GLIB_004:def 13

for e1 being set holds

( e1 in it iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) );

existence for e1 being set holds

( e1 in it iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) );

ex b

for e1 being set holds

( e1 in b

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) )

proof end;

uniqueness for b

( e1 in b

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) & ( for e1 being set holds

( e1 in b

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) holds

b

proof end;

:: deftheorem Def13 defines PRIM:NextBestEdges GLIB_004:def 13 :

for G being real-weighted WGraph

for L being PRIM:Labeling of G

for b_{3} being Subset of (the_Edges_of G) holds

( b_{3} = PRIM:NextBestEdges L iff for e1 being set holds

( e1 in b_{3} iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1),G holds

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) );

for G being real-weighted WGraph

for L being PRIM:Labeling of G

for b

( b

( e1 in b

(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) );

definition

let G be real-weighted WGraph;

[{ the Element of the_Vertices_of G},{}] is PRIM:Labeling of G

end;
func PRIM:Init G -> PRIM:Labeling of G equals :: GLIB_004:def 14

[{ the Element of the_Vertices_of G},{}];

coherence [{ the Element of the_Vertices_of G},{}];

[{ the Element of the_Vertices_of G},{}] is PRIM:Labeling of G

proof end;

:: deftheorem defines PRIM:Init GLIB_004:def 14 :

for G being real-weighted WGraph holds PRIM:Init G = [{ the Element of the_Vertices_of G},{}];

for G being real-weighted WGraph holds PRIM:Init G = [{ the Element of the_Vertices_of G},{}];

definition

let G be real-weighted WGraph;

let L be PRIM:Labeling of G;

( ( PRIM:NextBestEdges L = {} implies L is PRIM:Labeling of G ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 implies [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ) implies [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G ) )

for b_{1} being PRIM:Labeling of G st PRIM:NextBestEdges L = {} & PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 holds

( b_{1} = L iff b_{1} = [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )
;

end;
let L be PRIM:Labeling of G;

func PRIM:Step L -> PRIM:Labeling of G equals :Def15: :: GLIB_004:def 15

L if PRIM:NextBestEdges L = {}

[((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] if ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 )

otherwise [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})];

coherence L if PRIM:NextBestEdges L = {}

[((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] if ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 )

otherwise [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})];

( ( PRIM:NextBestEdges L = {} implies L is PRIM:Labeling of G ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 implies [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ) implies [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] is PRIM:Labeling of G ) )

proof end;

consistency for b

( b

:: deftheorem Def15 defines PRIM:Step GLIB_004:def 15 :

for G being real-weighted WGraph

for L being PRIM:Labeling of G holds

( ( PRIM:NextBestEdges L = {} implies PRIM:Step L = L ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 implies PRIM:Step L = [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ) implies PRIM:Step L = [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] ) );

for G being real-weighted WGraph

for L being PRIM:Labeling of G holds

( ( PRIM:NextBestEdges L = {} implies PRIM:Step L = L ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 implies PRIM:Step L = [((L `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . the Element of PRIM:NextBestEdges L in L `1 ) implies PRIM:Step L = [((L `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges L)}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] ) );

definition

let G be real-weighted WGraph;

ex b_{1} being ManySortedSet of NAT st

for n being Nat holds b_{1} . n is PRIM:Labeling of G

end;
mode PRIM:LabelingSeq of G -> ManySortedSet of NAT means :Def16: :: GLIB_004:def 16

for n being Nat holds it . n is PRIM:Labeling of G;

existence for n being Nat holds it . n is PRIM:Labeling of G;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def16 defines PRIM:LabelingSeq GLIB_004:def 16 :

for G being real-weighted WGraph

for b_{2} being ManySortedSet of NAT holds

( b_{2} is PRIM:LabelingSeq of G iff for n being Nat holds b_{2} . n is PRIM:Labeling of G );

for G being real-weighted WGraph

for b

( b

definition

let G be real-weighted WGraph;

let S be PRIM:LabelingSeq of G;

let n be Nat;

:: original: .

redefine func S . n -> PRIM:Labeling of G;

coherence

S . n is PRIM:Labeling of G by Def16;

end;
let S be PRIM:LabelingSeq of G;

let n be Nat;

:: original: .

redefine func S . n -> PRIM:Labeling of G;

coherence

S . n is PRIM:Labeling of G by Def16;

definition

let G be real-weighted WGraph;

ex b_{1} being PRIM:LabelingSeq of G st

( b_{1} . 0 = PRIM:Init G & ( for n being Nat holds b_{1} . (n + 1) = PRIM:Step (b_{1} . n) ) )

for b_{1}, b_{2} being PRIM:LabelingSeq of G st b_{1} . 0 = PRIM:Init G & ( for n being Nat holds b_{1} . (n + 1) = PRIM:Step (b_{1} . n) ) & b_{2} . 0 = PRIM:Init G & ( for n being Nat holds b_{2} . (n + 1) = PRIM:Step (b_{2} . n) ) holds

b_{1} = b_{2}

end;
func PRIM:CompSeq G -> PRIM:LabelingSeq of G means :Def17: :: GLIB_004:def 17

( it . 0 = PRIM:Init G & ( for n being Nat holds it . (n + 1) = PRIM:Step (it . n) ) );

existence ( it . 0 = PRIM:Init G & ( for n being Nat holds it . (n + 1) = PRIM:Step (it . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def17 defines PRIM:CompSeq GLIB_004:def 17 :

for G being real-weighted WGraph

for b_{2} being PRIM:LabelingSeq of G holds

( b_{2} = PRIM:CompSeq G iff ( b_{2} . 0 = PRIM:Init G & ( for n being Nat holds b_{2} . (n + 1) = PRIM:Step (b_{2} . n) ) ) );

for G being real-weighted WGraph

for b

( b

definition

let G be real-weighted WGraph;

coherence

(PRIM:CompSeq G) .Result() is PRIM:Labeling of G

end;
coherence

(PRIM:CompSeq G) .Result() is PRIM:Labeling of G

proof end;

:: deftheorem defines PRIM:MST GLIB_004:def 18 :

for G being real-weighted WGraph holds PRIM:MST G = (PRIM:CompSeq G) .Result() ;

for G being real-weighted WGraph holds PRIM:MST G = (PRIM:CompSeq G) .Result() ;

theorem Th28: :: GLIB_004:28

for G being real-weighted WGraph

for L being PRIM:Labeling of G st PRIM:NextBestEdges L <> {} holds

ex v being Vertex of G st

( not v in L `1 & PRIM:Step L = [((L `1) \/ {v}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )

for L being PRIM:Labeling of G st PRIM:NextBestEdges L <> {} holds

ex v being Vertex of G st

( not v in L `1 & PRIM:Step L = [((L `1) \/ {v}),((L `2) \/ { the Element of PRIM:NextBestEdges L})] )

proof end;

theorem Th29: :: GLIB_004:29

for G being real-weighted WGraph

for L being PRIM:Labeling of G holds

( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )

for L being PRIM:Labeling of G holds

( L `1 c= (PRIM:Step L) `1 & L `2 c= (PRIM:Step L) `2 )

proof end;

theorem Th30: :: GLIB_004:30

for G being finite real-weighted WGraph

for n being Nat holds

( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1) )

for n being Nat holds

( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1) )

proof end;

theorem Th31: :: GLIB_004:31

for G1 being finite real-weighted WGraph

for n being Nat

for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is connected

for n being Nat

for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is connected

proof end;

theorem Th32: :: GLIB_004:32

for G1 being finite real-weighted WGraph

for n being Nat

for G2 being inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1) holds G2 is connected

for n being Nat

for G2 being inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1) holds G2 is connected

proof end;

registration

let G1 be finite real-weighted WGraph;

let n be Nat;

for b_{1} being inducedSubgraph of G1,(((PRIM:CompSeq G1) . n) `1) holds b_{1} is connected
by Th32;

end;
let n be Nat;

cluster -> connected for inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,G1 .edgesBetween (((PRIM:CompSeq G1) . n) `1);

coherence for b

registration

let G1 be finite real-weighted WGraph;

let n be Nat;

for b_{1} being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds b_{1} is connected
by Th31;

end;
let n be Nat;

cluster -> connected for inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 ;

coherence for b

theorem Th33: :: GLIB_004:33

for G being finite real-weighted WGraph

for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G

for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G

proof end;

theorem Th34: :: GLIB_004:34

for G being finite real-weighted WGraph

for i, j being Nat st i <= j holds

( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )

for i, j being Nat st i <= j holds

( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )

proof end;

theorem Th35: :: GLIB_004:35

for G being finite real-weighted WGraph

for n being Nat holds

( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} iff ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G )

for n being Nat holds

( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} iff ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G )

proof end;

theorem Th36: :: GLIB_004:36

for G being finite real-weighted WGraph

for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G)))

for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G)))

proof end;

theorem Th37: :: GLIB_004:37

for G being finite real-weighted WGraph holds

( PRIM:CompSeq G is halting & ((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G) )

( PRIM:CompSeq G is halting & ((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G) )

proof end;

theorem Th38: :: GLIB_004:38

for G1 being finite real-weighted WGraph

for n being Nat

for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is Tree-like

for n being Nat

for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is Tree-like

proof end;

registration

let G be finite connected real-weighted WGraph;

ex b_{1} being WSubgraph of G st

( b_{1} is spanning & b_{1} is Tree-like )

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

existence ex b

( b

proof end;

definition
end;

:: deftheorem Def19 defines min-cost GLIB_004:def 19 :

for G1 being finite connected real-weighted WGraph

for G2 being spanning Tree-like WSubgraph of G1 holds

( G2 is min-cost iff for G3 being spanning Tree-like WSubgraph of G1 holds G2 .cost() <= G3 .cost() );

for G1 being finite connected real-weighted WGraph

for G2 being spanning Tree-like WSubgraph of G1 holds

( G2 is min-cost iff for G3 being spanning Tree-like WSubgraph of G1 holds G2 .cost() <= G3 .cost() );

registration

let G1 be finite connected real-weighted WGraph;

ex b_{1} being spanning Tree-like WSubgraph of G1 st b_{1} is min-cost

end;
cluster Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite loopless non-multi non-Dmulti simple Dsimple spanning connected acyclic Tree-like [Weighted] weight-inheriting real-weighted min-cost for Subgraph of G1;

existence ex b

proof end;

definition

let G be finite connected real-weighted WGraph;

mode minimumSpanningTree of G is spanning Tree-like min-cost WSubgraph of G;

end;
mode minimumSpanningTree of G is spanning Tree-like min-cost WSubgraph of G;

theorem :: GLIB_004:40

for G1, G2 being finite connected real-weighted WGraph

for G3 being WSubgraph of G1 st G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds

G3 is minimumSpanningTree of G2

for G3 being WSubgraph of G1 st G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds

G3 is minimumSpanningTree of G2

proof end;

theorem Th41: :: GLIB_004:41

for G being finite connected real-weighted WGraph

for G1 being minimumSpanningTree of G

for G2 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds

G2 is minimumSpanningTree of G

for G1 being minimumSpanningTree of G

for G2 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds

G2 is minimumSpanningTree of G

proof end;

theorem Th42: :: GLIB_004:42

for G being finite connected real-weighted WGraph

for n being Nat holds ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2

for n being Nat holds ((PRIM:CompSeq G) . n) `2 c= (PRIM:MST G) `2

proof end;

theorem :: GLIB_004:43

for G1 being finite connected real-weighted WGraph

for G2 being inducedWSubgraph of G1,(PRIM:MST G1) `1 ,(PRIM:MST G1) `2 holds G2 is minimumSpanningTree of G1

for G2 being inducedWSubgraph of G1,(PRIM:MST G1) `1 ,(PRIM:MST G1) `2 holds G2 is minimumSpanningTree of G1

proof end;