:: Proof of Dijkstra's Shortest Path Algorithm & Prim's Minimum Spanning Tree Algorithm
:: by Gilbert Lee and Piotr Rudnicki
::
:: Copyright (c) 2005-2018 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 Th1: :: GLIB_004:1
for f, g being Function holds support (f +* g) c= () \/ ()
proof end;

theorem Th2: :: GLIB_004:2
for f being Function
for x, y being object holds support (f +* (x .--> y)) c= () \/ {x}
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)
proof end;

theorem Th4: :: GLIB_004:4
for X, x being set
for b being Rbag of X st dom b = {x} holds
Sum b = b . x
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
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
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
proof end;

theorem Th8: :: GLIB_004:8
for X, x being set
for b being Rbag of X
for y being Real st b = () +* (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)
proof end;

definition
let G1 be real-weighted WGraph;
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() ) ) ) );
end;

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

definition
let G be real-weighted WGraph;
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() ) );
end;

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

definition
let G be finite real-weighted WGraph;
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 DWalk of G st W is_Walk_from x,y implies ex b1 being Real ex W being DPath of G st
( W is_mincost_DPath_from x,y & b1 = W .cost() ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ex b1 being Real st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 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 & b1 = W .cost() ) & ex W being DPath of G st
( W is_mincost_DPath_from x,y & b2 = W .cost() ) implies b1 = b2 ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Real holds verum
;
end;

:: deftheorem Def3 defines .min_DPath_cost GLIB_004:def 3 :
for G being finite real-weighted WGraph
for x, y being set
for b4 being Real holds
( ( ex W being DWalk of G st W is_Walk_from x,y implies ( b4 = G .min_DPath_cost (x,y) iff ex W being DPath of G st
( W is_mincost_DPath_from x,y & b4 = W .cost() ) ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ( b4 = G .min_DPath_cost (x,y) iff b4 = 0 ) ) );

definition
coherence ;
end;

Lm3: for G being WGraph holds WGraphSelectors c= dom G
proof end;

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

Lm4: for G being WGraph holds
( G == G | WGraphSelectors & the_Weight_of G = the_Weight_of () )

proof end;

Lm5: for G being WGraph holds dom () = WGraphSelectors
proof end;

definition
let G be WGraph;
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
ex b1 being non empty set st
for x being set holds
( x in b1 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) )
proof end;
uniqueness
for b1, b2 being non empty set st ( for x being set holds
( x in b1 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) ) & ( for x being set holds
( x in b2 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines .allWSubgraphs() GLIB_004:def 5 :
for G being WGraph
for b2 being non empty set holds
( b2 = G .allWSubgraphs() iff for x being set holds
( x in b2 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) );

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

definition
let G be WGraph;
let X be non empty Subset of ();
:: original: Element
redefine mode Element of X -> WSubgraph of G;
coherence
for b1 being Element of X holds b1 is WSubgraph of G
proof end;
end;

definition
let G be finite real-weighted WGraph;
func G .cost() -> Real equals :: GLIB_004:def 6
Sum ();
coherence
Sum () is Real
;
end;

:: deftheorem defines .cost() GLIB_004:def 6 :
for G being finite real-weighted WGraph holds G .cost() = Sum ();

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()) + (() . e)
proof end;

theorem Th11: :: GLIB_004:11
for G being finite real-weighted WGraph
for V1 being non empty Subset of ()
for E1 being Subset of ()
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()) + (() . 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()
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()
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;

definition
let G be _Graph;
mode DIJK:Labeling of G is Element of [:(PFuncs ((),REAL)),(bool ()):];
end;

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;

registration
let G be finite _Graph;
let L be DIJK:Labeling of G;
cluster K13(L) -> finite for set ;
coherence
for b1 being set st b1 = L 1 holds
b1 is finite
proof end;
cluster K14(L) -> finite for set ;
coherence
for b1 being set st b1 = L 2 holds
b1 is finite
;
end;

definition
let G be real-weighted WGraph;
let L be DIJK:Labeling of G;
func DIJK:NextBestEdges L -> Subset of () means :Def7: :: GLIB_004:def 7
for e1 being set holds
( e1 in it iff ( e1 DSJoins dom (L 1),() \ (dom (L 1)),G & ( for e2 being set st e2 DSJoins dom (L 1),() \ (dom (L 1)),G holds
((L 1) . (() . e1)) + (() . e1) <= ((L 1) . (() . e2)) + (() . e2) ) ) );
existence
ex b1 being Subset of () st
for e1 being set holds
( e1 in b1 iff ( e1 DSJoins dom (L 1),() \ (dom (L 1)),G & ( for e2 being set st e2 DSJoins dom (L 1),() \ (dom (L 1)),G holds
((L 1) . (() . e1)) + (() . e1) <= ((L 1) . (() . e2)) + (() . e2) ) ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for e1 being set holds
( e1 in b1 iff ( e1 DSJoins dom (L 1),() \ (dom (L 1)),G & ( for e2 being set st e2 DSJoins dom (L 1),() \ (dom (L 1)),G holds
((L 1) . (() . e1)) + (() . e1) <= ((L 1) . (() . e2)) + (() . e2) ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 DSJoins dom (L 1),() \ (dom (L 1)),G & ( for e2 being set st e2 DSJoins dom (L 1),() \ (dom (L 1)),G holds
((L 1) . (() . e1)) + (() . e1) <= ((L 1) . (() . e2)) + (() . e2) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines DIJK:NextBestEdges GLIB_004:def 7 :
for G being real-weighted WGraph
for L being DIJK:Labeling of G
for b3 being Subset of () holds
( b3 = DIJK:NextBestEdges L iff for e1 being set holds
( e1 in b3 iff ( e1 DSJoins dom (L 1),() \ (dom (L 1)),G & ( for e2 being set st e2 DSJoins dom (L 1),() \ (dom (L 1)),G holds
((L 1) . (() . e1)) + (() . e1) <= ((L 1) . (() . e2)) + (() . e2) ) ) ) );

definition
let G be real-weighted WGraph;
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 Element of DIJK:NextBestEdges L) .--> (((L 1) . (() . the Element of DIJK:NextBestEdges L)) + (() . the Element of DIJK:NextBestEdges L)))),((L 2) \/ {})];
coherence
( ( DIJK:NextBestEdges L = {} implies L is DIJK:Labeling of G ) & ( not DIJK:NextBestEdges L = {} implies [((L 1) +* ((() . the Element of DIJK:NextBestEdges L) .--> (((L 1) . (() . the Element of DIJK:NextBestEdges L)) + (() . the Element of DIJK:NextBestEdges L)))),((L 2) \/ {})] is DIJK:Labeling of G ) )
proof end;
consistency
for b1 being DIJK:Labeling of G holds verum
;
end;

:: 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 Element of DIJK:NextBestEdges L) .--> (((L 1) . (() . the Element of DIJK:NextBestEdges L)) + (() . the Element of DIJK:NextBestEdges L)))),((L 2) \/ {})] ) );

definition
let G be real-weighted WGraph;
let src be Vertex of G;
func DIJK:Init src -> DIJK:Labeling of G equals :: GLIB_004:def 9
[(src .--> 0),{}];
coherence
[(src .--> 0),{}] is DIJK:Labeling of G
proof end;
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),{}];

definition
let G be real-weighted WGraph;
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
ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n is DIJK:Labeling of G
proof end;
end;

:: deftheorem Def10 defines DIJK:LabelingSeq GLIB_004:def 10 :
for G being real-weighted WGraph
for b2 being ManySortedSet of NAT holds
( b2 is DIJK:LabelingSeq of G iff for n being Nat holds b2 . n is DIJK:Labeling of G );

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;

definition
let G be real-weighted WGraph;
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
ex b1 being DIJK:LabelingSeq of G st
( b1 . 0 = DIJK:Init src & ( for n being Nat holds b1 . (n + 1) = DIJK:Step (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being DIJK:LabelingSeq of G st b1 . 0 = DIJK:Init src & ( for n being Nat holds b1 . (n + 1) = DIJK:Step (b1 . n) ) & b2 . 0 = DIJK:Init src & ( for n being Nat holds b2 . (n + 1) = DIJK:Step (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines DIJK:CompSeq GLIB_004:def 11 :
for G being real-weighted WGraph
for src being Vertex of G
for b3 being DIJK:LabelingSeq of G holds
( b3 = DIJK:CompSeq src iff ( b3 . 0 = DIJK:Init src & ( for n being Nat holds b3 . (n + 1) = DIJK:Step (b3 . n) ) ) );

definition
let G be real-weighted WGraph;
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() is DIJK:Labeling of G
proof end;
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() ;

theorem Th15: :: GLIB_004:15
for G being finite real-weighted WGraph
for L being DIJK:Labeling of G holds
( ( card (dom (() 1)) = card (dom (L 1)) implies DIJK:NextBestEdges L = {} ) & ( DIJK:NextBestEdges L = {} implies card (dom (() 1)) = card (dom (L 1)) ) & ( card (dom (() 1)) = (card (dom (L 1))) + 1 implies DIJK:NextBestEdges L <> {} ) & ( DIJK:NextBestEdges L <> {} implies card (dom (() 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 (() 1) & L 2 c= () 2 )
proof end;

theorem Th17: :: GLIB_004:17
for G being real-weighted WGraph
for src being Vertex of G holds dom ((DIJK:Init src) 1) = {src}
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 )
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
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 )
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 ((() . n) 1)) = min ((n + 1),(card ()))
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))
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 ((() . n) 1),(() . n) 2 holds
( G2 is_mincost_DTree_rooted_at s & ( for v being Vertex of G st v in dom ((() . n) 1) holds
G .min_DPath_cost (s,v) = ((() . n) 1) . v ) )
proof end;

theorem Th24: :: GLIB_004:24
for G being finite real-weighted WGraph
for s being Vertex of G holds DIJK:CompSeq s is halting
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;

theorem Th25: :: GLIB_004:25
for G being finite real-weighted WGraph
for s being Vertex of G holds () + 1 = card ()
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
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 ) ) )
proof end;

definition
let G be _Graph;
mode PRIM:Labeling of G is Element of [:(),(bool ()):];
end;

registration
let G be finite _Graph;
let L be PRIM:Labeling of G;
cluster K13(L) -> finite for set ;
coherence
for b1 being set st b1 = L 1 holds
b1 is finite
;
cluster K14(L) -> finite for set ;
coherence
for b1 being set st b1 = L 2 holds
b1 is finite
;
end;

definition
let G be real-weighted WGraph;
let L be PRIM:Labeling of G;
func PRIM:NextBestEdges L -> Subset of () means :Def13: :: GLIB_004:def 13
for e1 being set holds
( e1 in it iff ( e1 SJoins L 1 ,() \ (L 1),G & ( for e2 being set st e2 SJoins L 1 ,() \ (L 1),G holds
() . e1 <= () . e2 ) ) );
existence
ex b1 being Subset of () st
for e1 being set holds
( e1 in b1 iff ( e1 SJoins L 1 ,() \ (L 1),G & ( for e2 being set st e2 SJoins L 1 ,() \ (L 1),G holds
() . e1 <= () . e2 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for e1 being set holds
( e1 in b1 iff ( e1 SJoins L 1 ,() \ (L 1),G & ( for e2 being set st e2 SJoins L 1 ,() \ (L 1),G holds
() . e1 <= () . e2 ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 SJoins L 1 ,() \ (L 1),G & ( for e2 being set st e2 SJoins L 1 ,() \ (L 1),G holds
() . e1 <= () . e2 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines PRIM:NextBestEdges GLIB_004:def 13 :
for G being real-weighted WGraph
for L being PRIM:Labeling of G
for b3 being Subset of () holds
( b3 = PRIM:NextBestEdges L iff for e1 being set holds
( e1 in b3 iff ( e1 SJoins L 1 ,() \ (L 1),G & ( for e2 being set st e2 SJoins L 1 ,() \ (L 1),G holds
() . e1 <= () . e2 ) ) ) );

definition
let G be real-weighted WGraph;
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},{}] is PRIM:Labeling of G
proof end;
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},{}];

definition
let G be real-weighted WGraph;
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 Element of PRIM:NextBestEdges L)}),((L 2) \/ {})] if ( PRIM:NextBestEdges L <> {} & () . the Element of PRIM:NextBestEdges L in L 1 )
otherwise [((L 1) \/ {(() . the Element of PRIM:NextBestEdges L)}),((L 2) \/ {})];
coherence
( ( PRIM:NextBestEdges L = {} implies L is PRIM:Labeling of G ) & ( PRIM:NextBestEdges L <> {} & () . the Element of PRIM:NextBestEdges L in L 1 implies [((L 1) \/ {(() . the Element of PRIM:NextBestEdges L)}),((L 2) \/ {})] is PRIM:Labeling of G ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not () . the Element of PRIM:NextBestEdges L in L 1 ) implies [((L 1) \/ {(() . the Element of PRIM:NextBestEdges L)}),((L 2) \/ {})] is PRIM:Labeling of G ) )
proof end;
consistency
for b1 being PRIM:Labeling of G st PRIM:NextBestEdges L = {} & PRIM:NextBestEdges L <> {} & () . the Element of PRIM:NextBestEdges L in L 1 holds
( b1 = L iff b1 = [((L 1) \/ {(() . the Element of PRIM:NextBestEdges L)}),((L 2) \/ {})] )
;
end;

:: 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 Element of PRIM:NextBestEdges L in L 1 implies PRIM:Step L = [((L 1) \/ {(() . the Element of PRIM:NextBestEdges L)}),((L 2) \/ {})] ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not () . the Element of PRIM:NextBestEdges L in L 1 ) implies PRIM:Step L = [((L 1) \/ {(() . the Element of PRIM:NextBestEdges L)}),((L 2) \/ {})] ) );

definition
let G be real-weighted WGraph;
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
ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n is PRIM:Labeling of G
proof end;
end;

:: deftheorem Def16 defines PRIM:LabelingSeq GLIB_004:def 16 :
for G being real-weighted WGraph
for b2 being ManySortedSet of NAT holds
( b2 is PRIM:LabelingSeq of G iff for n being Nat holds b2 . n is PRIM:Labeling of G );

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;

definition
let G be real-weighted WGraph;
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
ex b1 being PRIM:LabelingSeq of G st
( b1 . 0 = PRIM:Init G & ( for n being Nat holds b1 . (n + 1) = PRIM:Step (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being PRIM:LabelingSeq of G st b1 . 0 = PRIM:Init G & ( for n being Nat holds b1 . (n + 1) = PRIM:Step (b1 . n) ) & b2 . 0 = PRIM:Init G & ( for n being Nat holds b2 . (n + 1) = PRIM:Step (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines PRIM:CompSeq GLIB_004:def 17 :
for G being real-weighted WGraph
for b2 being PRIM:LabelingSeq of G holds
( b2 = PRIM:CompSeq G iff ( b2 . 0 = PRIM:Init G & ( for n being Nat holds b2 . (n + 1) = PRIM:Step (b2 . n) ) ) );

definition
let G be real-weighted WGraph;
func PRIM:MST G -> PRIM:Labeling of G equals :: GLIB_004:def 18
() .Result() ;
coherence
() .Result() is PRIM:Labeling of G
proof end;
end;

:: deftheorem defines PRIM:MST GLIB_004:def 18 :
for G being real-weighted WGraph holds PRIM:MST 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) \/ {})] )
proof end;

theorem Th29: :: GLIB_004:29
for G being real-weighted WGraph
for L being PRIM:Labeling of G holds
( L 1 c= () 1 & L 2 c= () 2 )
proof end;

theorem Th30: :: GLIB_004:30
for G being finite real-weighted WGraph
for n being Nat holds
( (() . n) 1 is non empty Subset of () & (() . n) 2 c= G .edgesBetween ((() . 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,(() . n) 1 ,(() . 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,((() . n) 1) holds G2 is connected
proof end;

registration
let G1 be finite real-weighted WGraph;
let n be Nat;
cluster -> connected for inducedSubgraph of G1,((() . n) 1);
coherence
for b1 being inducedSubgraph of G1,((() . n) 1) holds b1 is connected
by Th32;
end;

registration
let G1 be finite real-weighted WGraph;
let n be Nat;
cluster -> connected for inducedSubgraph of G1,(() . n) 1 ,(() . n) 2 ;
coherence
for b1 being inducedSubgraph of G1,(() . n) 1 ,(() . n) 2 holds b1 is connected
by Th31;
end;

theorem Th33: :: GLIB_004:33
for G being finite real-weighted WGraph
for n being Nat holds (() . 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
( (() . i) 1 c= (() . j) 1 & (() . i) 2 c= (() . j) 2 )
proof end;

theorem Th35: :: GLIB_004:35
for G being finite real-weighted WGraph
for n being Nat holds
( PRIM:NextBestEdges (() . n) = {} iff (() . 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 ((() . n) 1) = min ((n + 1),(card ()))
proof end;

theorem Th37: :: GLIB_004:37
for G being finite real-weighted WGraph holds
( PRIM:CompSeq G is halting & () + 1 = card () )
proof end;

theorem Th38: :: GLIB_004:38
for G1 being finite real-weighted WGraph
for n being Nat
for G2 being inducedSubgraph of G1,(() . n) 1 ,(() . n) 2 holds G2 is Tree-like
proof end;

theorem Th39: :: GLIB_004:39
for G being finite connected real-weighted WGraph holds () 1 = the_Vertices_of G
proof end;

registration
let G be finite connected real-weighted WGraph;
existence
ex b1 being WSubgraph of G st
( b1 is spanning & b1 is Tree-like )
proof end;
end;

definition
let G1 be finite connected real-weighted WGraph;
let G2 be spanning Tree-like WSubgraph of G1;
attr G2 is min-cost means :Def19: :: GLIB_004:def 19
for G3 being spanning Tree-like WSubgraph of G1 holds G2 .cost() <= G3 .cost() ;
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() );

registration
let G1 be finite connected real-weighted WGraph;
existence
ex b1 being spanning Tree-like WSubgraph of G1 st b1 is min-cost
proof end;
end;

definition end;

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

theorem Th42: :: GLIB_004:42
for G being finite connected real-weighted WGraph
for n being Nat holds (() . n) 2 c= () 2
proof end;

:: Prim's Minimum Spanning Tree Algorithm
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
proof end;