:: GLIB_004 semantic presentation

theorem Th1: :: GLIB_004:1

for b₁, b₂ being Function holds support (b₁ +* b₂) c= (support b₁) \/ (support b₂)

proof end;

theorem Th2: :: GLIB_004:2

for b₁ being Function
for b₂, b₃ being set holds support (b₁ +* (b₂ .--> b₃)) c= (support b₁) \/ {b₂}

proof end;

theorem Th3: :: GLIB_004:3

for b₁, b₂ being set
for b₃ being Rbag of b₁
for b₄ being Rbag of b₂
for b₅ being Rbag of b₁ \ b₂ st b₃ = b₄ +* b₅ holds
Sum b₃ = (Sum b₄) + (Sum b₅)

proof end;

theorem Th4: :: GLIB_004:4

for b₁, b₂ being set
for b₃ being Rbag of b₁ st dom b₃ = {b₂} holds
Sum b₃ = b₃ . b₂

proof end;

theorem Th5: :: GLIB_004:5

for b₁ being set
for b₂, b₃ being Rbag of b₁ st ( for b₄ being set st b₄ in b₁ holds
b₂ . b₄ <= b₃ . b₄ ) holds
Sum b₂ <= Sum b₃

proof end;

theorem Th6: :: GLIB_004:6

for b₁ being set
for b₂, b₃ being Rbag of b₁ st ( for b₄ being set st b₄ in b₁ holds
b₂ . b₄ = b₃ . b₄ ) holds
Sum b₂ = Sum b₃

proof end;

theorem Th7: :: GLIB_004:7

for b₁, b₂ being set
for b₃ being Rbag of b₁
for b₄ being Rbag of b₂ st b₃ = b₄ holds
Sum b₃ = Sum b₄

proof end;

theorem Th8: :: GLIB_004:8

for b₁, b₂ being set
for b₃ being Rbag of b₁
for b₄ being real number st b₃ = (EmptyBag b₁) +* (b₂ .--> b₄) holds
Sum b₃ = b₄

proof end;

theorem Th9: :: GLIB_004:9

for b₁, b₂ being set
for b₃, b₄ being Rbag of b₁
for b₅ being real number st b₄ = b₃ +* (b₂ .--> b₅) holds
Sum b₄ = ((Sum b₃) + b₅) - (b₃ . b₂)

proof end;

definition

let c₁ be real-weighted WGraph;
let c₂ be WSubgraph of c₁;
let c₃ be set ;
pred c₂ is_mincost_DTree_rooted_at c₃ means :Def1: :: GLIB_004:def 1
( a₂ is Tree-like & ( for b₁ being Vertex of a₂ ex b₂ being DPath of a₂ st
( b₂ is_Walk_from a₃,b₁ & ( for b₃ being DPath of a₁ st b₃ is_Walk_from a₃,b₁ holds
b₂ .cost() <= b₃ .cost() ) ) ) );

end;

:: deftheorem Def1 defines is_mincost_DTree_rooted_at GLIB_004:def 1 :

definition

let c₁ be real-weighted WGraph;
let c₂ be DPath of c₁;
let c₃, c₄ be set ;
pred c₂ is_mincost_DPath_from c₃,c₄ means :Def2: :: GLIB_004:def 2
( a₂ is_Walk_from a₃,a₄ & ( for b₁ being DPath of a₁ st b₁ is_Walk_from a₃,a₄ holds
a₂ .cost() <= b₁ .cost() ) );

end;

:: deftheorem Def2 defines is_mincost_DPath_from GLIB_004:def 2 :

definition

let c₁ be finite real-weighted WGraph;
let c₂, c₃ be set ;
func c₁ .min_DPath_cost c₂,c₃ -> Real means :Def3: :: GLIB_004:def 3
ex b₁ being DPath of a₁ st
( b₁ is_mincost_DPath_from a₂,a₃ & a₄ = b₁ .cost() ) if ex b₁ being DWalk of a₁ st b₁ is_Walk_from a₂,a₃
otherwise a₄ = 0;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

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

definition

let c₁ be real-WEV WEVGraph;
func DIJK:NextBestEdges c₁ -> Subset of (the_Edges_of a₁) means :Def4: :: GLIB_004:def 4
for b₁ being set holds
( b₁ in a₂ iff ( b₁ DSJoins a₁ .labeledV() ,(the_Vertices_of a₁) \ (a₁ .labeledV() ),a₁ & ( for b₂ being set st b₂ DSJoins a₁ .labeledV() ,(the_Vertices_of a₁) \ (a₁ .labeledV() ),a₁ holds
((the_VLabel_of a₁) . ((the_Source_of a₁) . b₁)) + ((the_Weight_of a₁) . b₁) <= ((the_VLabel_of a₁) . ((the_Source_of a₁) . b₂)) + ((the_Weight_of a₁) . b₂) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines DIJK:NextBestEdges GLIB_004:def 4 :

definition

let c₁ be real-WEV WEVGraph;
set c₂ = choose (DIJK:NextBestEdges c₁);
func DIJK:Step c₁ -> real-WEV WEVGraph equals :Def5: :: GLIB_004:def 5
a₁ if DIJK:NextBestEdges a₁ = {}
otherwise (a₁ .labelEdge (choose (DIJK:NextBestEdges a₁)),1) .labelVertex ((the_Target_of a₁) . (choose (DIJK:NextBestEdges a₁))),(((the_VLabel_of a₁) . ((the_Source_of a₁) . (choose (DIJK:NextBestEdges a₁)))) + ((the_Weight_of a₁) . (choose (DIJK:NextBestEdges a₁))));
coherence ;
consistency ;

end;

:: deftheorem Def5 defines DIJK:Step GLIB_004:def 5 :

registration

let c₁ be finite real-WEV WEVGraph;
cluster DIJK:Step a₁ -> finite real-WEV ;
coherence

proof end;

end;

registration

let c₁ be nonnegative-weighted real-WEV WEVGraph;
cluster DIJK:Step a₁ -> nonnegative-weighted real-WEV ;
coherence

proof end;

end;

definition

let c₁ be real-weighted WGraph;
let c₂ be Vertex of c₁;
func DIJK:Init c₁,c₂ -> real-WEV WEVGraph equals :: GLIB_004:def 6
(a₁ .set ELabelSelector ,{} ) .set VLabelSelector ,(a₂ .--> 0);
coherence

proof end;

end;

:: deftheorem Def6 defines DIJK:Init GLIB_004:def 6 :

definition

let c₁ be real-weighted WGraph;
let c₂ be Vertex of c₁;
func DIJK:CompSeq c₁,c₂ -> real-WEV WEVGraphSeq means :Def7: :: GLIB_004:def 7
( a₃ .-> 0 = DIJK:Init a₁,a₂ & ( for b₁ being Nat holds a₃ .-> (b₁ + 1) = DIJK:Step (a₃ .-> b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let c₁ be finite real-weighted WGraph;
let c₂ be Vertex of c₁;
cluster DIJK:CompSeq a₁,a₂ -> finite real-WEV ;
coherence

proof end;

end;

registration

let c₁ be nonnegative-weighted WGraph;
let c₂ be Vertex of c₁;
cluster DIJK:CompSeq a₁,a₂ -> nonnegative-weighted real-WEV ;
coherence

proof end;

end;

definition

let c₁ be real-weighted WGraph;
let c₂ be Vertex of c₁;
func DIJK:SSSP c₁,c₂ -> real-WEV WEVGraph equals :: GLIB_004:def 8
(DIJK:CompSeq a₁,a₂) .Result() ;
coherence

proof end;

end;

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

registration

let c₁ be finite real-weighted WGraph;
let c₂ be Vertex of c₁;
cluster DIJK:SSSP a₁,a₂ -> finite real-WEV ;
coherence

proof end;

end;

theorem Th10: :: GLIB_004:10

for b₁ being finite nonnegative-weighted WGraph
for b₂ being DPath of b₁
for b₃, b₄ being set
for b₅, b₆ being Nat st b₂ is_mincost_DPath_from b₃,b₄ holds
b₂ .cut b₅,b₆ is_mincost_DPath_from (b₂ .cut b₅,b₆) .first() ,(b₂ .cut b₅,b₆) .last()

proof end;

theorem Th11: :: GLIB_004:11

for b₁ being finite real-weighted WGraph
for b₂, b₃ being DPath of b₁
for b₄, b₅ being set st b₂ is_mincost_DPath_from b₄,b₅ & b₃ is_mincost_DPath_from b₄,b₅ holds
b₂ .cost() = b₃ .cost()

proof end;

theorem Th12: :: GLIB_004:12

for b₁ being finite real-weighted WGraph
for b₂ being DPath of b₁
for b₃, b₄ being set st b₂ is_mincost_DPath_from b₃,b₄ holds
b₁ .min_DPath_cost b₃,b₄ = b₂ .cost()

proof end;

theorem Th13: :: GLIB_004:13

for b₁ being finite real-WEV WEVGraph holds
( ( card ((DIJK:Step b₁) .labeledV() ) = card (b₁ .labeledV() ) implies DIJK:NextBestEdges b₁ = {} ) & ( DIJK:NextBestEdges b₁ = {} implies card ((DIJK:Step b₁) .labeledV() ) = card (b₁ .labeledV() ) ) & ( card ((DIJK:Step b₁) .labeledV() ) = (card (b₁ .labeledV() )) + 1 implies DIJK:NextBestEdges b₁ <> {} ) & ( DIJK:NextBestEdges b₁ <> {} implies card ((DIJK:Step b₁) .labeledV() ) = (card (b₁ .labeledV() )) + 1 ) )

proof end;

theorem Th14: :: GLIB_004:14

for b₁ being real-WEV WEVGraph holds
( b₁ == DIJK:Step b₁ & the_Weight_of b₁ = the_Weight_of (DIJK:Step b₁) & b₁ .labeledE() c= (DIJK:Step b₁) .labeledE() & b₁ .labeledV() c= (DIJK:Step b₁) .labeledV() )

proof end;

theorem Th15: :: GLIB_004:15

for b₁ being real-weighted WGraph
for b₂ being Vertex of b₁ holds (DIJK:Init b₁,b₂) .labeledV() = {b₂}

proof end;

theorem Th16: :: GLIB_004:16

for b₁ being real-weighted WGraph
for b₂ being Vertex of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
( ((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() c= ((DIJK:CompSeq b₁,b₂) .-> b₄) .labeledV() & ((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledE() c= ((DIJK:CompSeq b₁,b₂) .-> b₄) .labeledE() )

proof end;

theorem Th17: :: GLIB_004:17

for b₁ being real-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being Nat holds
( b₁ == (DIJK:CompSeq b₁,b₂) .-> b₃ & the_Weight_of b₁ = the_Weight_of ((DIJK:CompSeq b₁,b₂) .-> b₃) )

proof end;

theorem Th18: :: GLIB_004:18

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being Nat holds ((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() c= b₁ .reachableDFrom b₂

proof end;

theorem Th19: :: GLIB_004:19

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being Nat holds
( DIJK:NextBestEdges ((DIJK:CompSeq b₁,b₂) .-> b₃) = {} iff ((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() = b₁ .reachableDFrom b₂ )

proof end;

theorem Th20: :: GLIB_004:20

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being Nat holds Card (((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() ) = min (b₃ + 1),(card (b₁ .reachableDFrom b₂))

proof end;

theorem Th21: :: GLIB_004:21

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being Nat holds ((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledE() c= ((DIJK:CompSeq b₁,b₂) .-> b₃) .edgesBetween (((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() )

proof end;

theorem Th22: :: GLIB_004:22

for b₁ being finite nonnegative-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being Nat
for b₄ being inducedWSubgraph of b₁,((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() ,((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledE() holds
( b₄ is_mincost_DTree_rooted_at b₂ & ( for b₅ being Vertex of b₁ st b₅ in ((DIJK:CompSeq b₁,b₂) .-> b₃) .labeledV() holds
b₁ .min_DPath_cost b₂,b₅ = (the_VLabel_of ((DIJK:CompSeq b₁,b₂) .-> b₃)) . b₅ ) )

proof end;

theorem Th23: :: GLIB_004:23

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁ holds DIJK:CompSeq b₁,b₂ is halting

proof end;

registration

let c₁ be finite real-weighted WGraph;
let c₂ be Vertex of c₁;
cluster DIJK:CompSeq a₁,a₂ -> halting finite real-WEV ;
coherence by Th23;

end;

theorem Th24: :: GLIB_004:24

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁ holds ((DIJK:CompSeq b₁,b₂) .Lifespan() ) + 1 = card (b₁ .reachableDFrom b₂)

proof end;

theorem Th25: :: GLIB_004:25

for b₁ being finite real-weighted WGraph
for b₂ being Vertex of b₁ holds (DIJK:SSSP b₁,b₂) .labeledV() = b₁ .reachableDFrom b₂

proof end;

theorem Th26: :: GLIB_004:26

for b₁ being finite nonnegative-weighted WGraph
for b₂ being Vertex of b₁
for b₃ being inducedWSubgraph of b₁,(DIJK:SSSP b₁,b₂) .labeledV() ,(DIJK:SSSP b₁,b₂) .labeledE() holds
( b₃ is_mincost_DTree_rooted_at b₂ & ( for b₄ being Vertex of b₁ st b₄ in b₁ .reachableDFrom b₂ holds
( b₄ in the_Vertices_of b₃ & b₁ .min_DPath_cost b₂,b₄ = (the_VLabel_of (DIJK:SSSP b₁,b₂)) . b₄ ) ) )

proof end;

definition

func WGraphSelectors -> non empty finite Subset of NAT equals :: GLIB_004:def 9
{VertexSelector ,EdgeSelector ,SourceSelector ,TargetSelector ,WeightSelector };
coherence by ENUMSET1:def 3;

end;

:: deftheorem Def9 defines WGraphSelectors GLIB_004:def 9 :

Lemma29: for b₁ being WGraph holds WGraphSelectors c= dom b₁

proof end;

registration

let c₁ be WGraph;
cluster a₁ .strict WGraphSelectors -> [Graph-like] [Weighted] ;
coherence

proof end;

end;

Lemma30: for b₁ being WGraph holds
( b₁ == b₁ .strict WGraphSelectors & the_Weight_of b₁ = the_Weight_of (b₁ .strict WGraphSelectors ) )

proof end;

Lemma31: for b₁ being WGraph holds dom (b₁ .strict WGraphSelectors ) = WGraphSelectors

proof end;

definition

let c₁ be WGraph;
func c₁ .allWSubgraphs() -> non empty set means :Def10: :: GLIB_004:def 10
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being WSubgraph of a₁ st
( b₁ = b₂ & dom b₂ = WGraphSelectors ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines .allWSubgraphs() GLIB_004:def 10 :

registration

let c₁ be finite WGraph;
cluster a₁ .allWSubgraphs() -> non empty finite ;
coherence

proof end;

end;

definition

let c₁ be WGraph;
let c₂ be non empty Subset of (c₁ .allWSubgraphs() );
redefine mode Element as Element of c₂ -> WSubgraph of a₁;
coherence

proof end;

end;

definition

let c₁ be finite real-weighted WGraph;
func c₁ .cost() -> Real equals :: GLIB_004:def 11
Sum (the_Weight_of a₁);
coherence by XREAL_0:def 1;

end;

:: deftheorem Def11 defines .cost() GLIB_004:def 11 :

theorem Th27: :: GLIB_004:27

for b₁ being set holds
( b₁ in WGraphSelectors iff ( b₁ = VertexSelector or b₁ = EdgeSelector or b₁ = SourceSelector or b₁ = TargetSelector or b₁ = WeightSelector ) ) by ENUMSET1:def 3;

theorem Th28: :: GLIB_004:28

for b₁ being WGraph holds WGraphSelectors c= dom b₁ by Lemma29;

theorem Th29: :: GLIB_004:29

for b₁ being WGraph holds
( b₁ == b₁ .strict WGraphSelectors & the_Weight_of b₁ = the_Weight_of (b₁ .strict WGraphSelectors ) ) by Lemma30;

theorem Th30: :: GLIB_004:30

for b₁ being WGraph holds dom (b₁ .strict WGraphSelectors ) = WGraphSelectors by Lemma31;

theorem Th31: :: GLIB_004:31

for b₁ being finite real-weighted WGraph st the_Edges_of b₁ = {} holds
b₁ .cost() = 0

proof end;

theorem Th32: :: GLIB_004:32

for b₁, b₂ being finite real-weighted WGraph st the_Edges_of b₁ = the_Edges_of b₂ & the_Weight_of b₁ = the_Weight_of b₂ holds
b₁ .cost() = b₂ .cost() ;

theorem Th33: :: GLIB_004:33

for b₁ being finite real-weighted WGraph
for b₂ being set
for b₃ being [Weighted] weight-inheriting removeEdge of b₁,b₂ st b₂ in the_Edges_of b₁ holds
b₁ .cost() = (b₃ .cost() ) + ((the_Weight_of b₁) . b₂)

proof end;

theorem Th34: :: GLIB_004:34

for b₁ being finite real-weighted WGraph
for b₂ being non empty Subset of (the_Vertices_of b₁)
for b₃ being Subset of (b₁ .edgesBetween b₂)
for b₄ being inducedWSubgraph of b₁,b₂,b₃
for b₅ being set
for b₆ being inducedWSubgraph of b₁,b₂,b₃ \/ {b₅} st not b₅ in b₃ & b₅ in b₁ .edgesBetween b₂ holds
(b₄ .cost() ) + ((the_Weight_of b₁) . b₅) = b₆ .cost()

proof end;

definition

let c₁ be real-weighted WVGraph;
func PRIM:NextBestEdges c₁ -> Subset of (the_Edges_of a₁) means :Def12: :: GLIB_004:def 12
for b₁ being set holds
( b₁ in a₂ iff ( b₁ SJoins a₁ .labeledV() ,(the_Vertices_of a₁) \ (a₁ .labeledV() ),a₁ & ( for b₂ being set st b₂ SJoins a₁ .labeledV() ,(the_Vertices_of a₁) \ (a₁ .labeledV() ),a₁ holds
(the_Weight_of a₁) . b₁ <= (the_Weight_of a₁) . b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines PRIM:NextBestEdges GLIB_004:def 12 :

definition

let c₁ be real-weighted WGraph;
func PRIM:Init c₁ -> real-WEV WEVGraph equals :: GLIB_004:def 13
(a₁ .set VLabelSelector ,((choose (the_Vertices_of a₁)) .--> 1)) .set ELabelSelector ,{} ;
coherence ;

end;

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

definition

let c₁ be real-WEV WEVGraph;
set c₂ = choose (PRIM:NextBestEdges c₁);
func PRIM:Step c₁ -> real-WEV WEVGraph equals :Def14: :: GLIB_004:def 14
a₁ if PRIM:NextBestEdges a₁ = {}
(a₁ .labelEdge (choose (PRIM:NextBestEdges a₁)),1) .labelVertex ((the_Target_of a₁) . (choose (PRIM:NextBestEdges a₁))),1 if ( PRIM:NextBestEdges a₁ <> {} & (the_Source_of a₁) . (choose (PRIM:NextBestEdges a₁)) in a₁ .labeledV() )
otherwise (a₁ .labelEdge (choose (PRIM:NextBestEdges a₁)),1) .labelVertex ((the_Source_of a₁) . (choose (PRIM:NextBestEdges a₁))),1;
coherence ;
consistency ;

end;

:: deftheorem Def14 defines PRIM:Step GLIB_004:def 14 :

definition

let c₁ be real-weighted WGraph;
func PRIM:CompSeq c₁ -> real-WEV WEVGraphSeq means :Def15: :: GLIB_004:def 15
( a₂ .-> 0 = PRIM:Init a₁ & ( for b₁ being Nat holds a₂ .-> (b₁ + 1) = PRIM:Step (a₂ .-> b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let c₁ be finite real-weighted WGraph;
cluster PRIM:CompSeq a₁ -> finite real-WEV ;
coherence

proof end;

end;

definition

let c₁ be real-weighted WGraph;
func PRIM:MST c₁ -> real-WEV WEVGraph equals :: GLIB_004:def 16
(PRIM:CompSeq a₁) .Result() ;
coherence

proof end;

end;

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

registration

let c₁ be finite real-weighted WGraph;
cluster PRIM:MST a₁ -> finite real-WEV ;
coherence

proof end;

end;

Lemma38: for b₁ being real-weighted WGraph holds
( b₁ == PRIM:Init b₁ & the_Weight_of b₁ = the_Weight_of (PRIM:Init b₁) & the_ELabel_of (PRIM:Init b₁) = {} & the_VLabel_of (PRIM:Init b₁) = (choose (the_Vertices_of b₁)) .--> 1 )

proof end;

Lemma39: for b₁ being real-weighted WGraph holds
( (PRIM:Init b₁) .labeledV() = {(choose (the_Vertices_of b₁))} & (PRIM:Init b₁) .labeledE() = {} )

proof end;

Lemma40: for b₁ being real-WEV WEVGraph st PRIM:NextBestEdges b₁ <> {} holds
ex b₂ being Vertex of b₁ st
( not b₂ in b₁ .labeledV() & PRIM:Step b₁ = (b₁ .labelEdge (choose (PRIM:NextBestEdges b₁)),1) .labelVertex b₂,1 )

proof end;

Lemma41: for b₁ being real-WEV WEVGraph holds
( b₁ == PRIM:Step b₁ & the_Weight_of b₁ = the_Weight_of (PRIM:Step b₁) & b₁ .labeledE() c= (PRIM:Step b₁) .labeledE() & b₁ .labeledV() c= (PRIM:Step b₁) .labeledV() )

proof end;

Lemma42: for b₁ being finite real-weighted WGraph
for b₂ being Nat holds
( b₁ == (PRIM:CompSeq b₁) .-> b₂ & the_Weight_of ((PRIM:CompSeq b₁) .-> b₂) = the_Weight_of b₁ )

proof end;

Lemma43: for b₁ being finite real-weighted WGraph
for b₂ being Nat holds
( ((PRIM:CompSeq b₁) .-> b₂) .labeledV() is non empty Subset of (the_Vertices_of b₁) & ((PRIM:CompSeq b₁) .-> b₂) .labeledE() c= b₁ .edgesBetween (((PRIM:CompSeq b₁) .-> b₂) .labeledV() ) )

proof end;

Lemma44: for b₁ being finite real-weighted WGraph
for b₂ being Nat
for b₃ being inducedSubgraph of b₁,((PRIM:CompSeq b₁) .-> b₂) .labeledV() ,((PRIM:CompSeq b₁) .-> b₂) .labeledE() holds b₃ is connected

proof end;

Lemma45: for b₁ being finite real-weighted WGraph
for b₂ being Nat
for b₃ being inducedSubgraph of b₁,(((PRIM:CompSeq b₁) .-> b₂) .labeledV() ) holds b₃ is connected

proof end;

registration

let c₁ be finite real-weighted WGraph;
let c₂ be Nat;
cluster -> connected inducedSubgraph of a₁,((PRIM:CompSeq a₁) .-> a₂) .labeledV() ,a₁ .edgesBetween (((PRIM:CompSeq a₁) .-> a₂) .labeledV() );
coherence by Lemma45;

end;

registration

let c₁ be finite real-weighted WGraph;
let c₂ be Nat;
cluster -> connected inducedSubgraph of a₁,((PRIM:CompSeq a₁) .-> a₂) .labeledV() ,((PRIM:CompSeq a₁) .-> a₂) .labeledE() ;
coherence by Lemma44;

end;

Lemma46: for b₁ being finite real-weighted WGraph
for b₂ being Nat holds ((PRIM:CompSeq b₁) .-> b₂) .labeledV() c= b₁ .reachableFrom (choose (the_Vertices_of b₁))

proof end;

Lemma47: for b₁ being finite real-weighted WGraph
for b₂, b₃ being Nat st b₂ <= b₃ holds
( ((PRIM:CompSeq b₁) .-> b₂) .labeledV() c= ((PRIM:CompSeq b₁) .-> b₃) .labeledV() & ((PRIM:CompSeq b₁) .-> b₂) .labeledE() c= ((PRIM:CompSeq b₁) .-> b₃) .labeledE() )

proof end;

Lemma48: for b₁ being finite real-weighted WGraph
for b₂ being Nat holds
( PRIM:NextBestEdges ((PRIM:CompSeq b₁) .-> b₂) = {} iff ((PRIM:CompSeq b₁) .-> b₂) .labeledV() = b₁ .reachableFrom (choose (the_Vertices_of b₁)) )

proof end;

Lemma49: for b₁ being finite real-weighted WGraph
for b₂ being Nat holds card (((PRIM:CompSeq b₁) .-> b₂) .labeledV() ) = min (b₂ + 1),(card (b₁ .reachableFrom (choose (the_Vertices_of b₁))))

proof end;

Lemma50: for b₁ being finite real-weighted WGraph holds
( PRIM:CompSeq b₁ is halting & ((PRIM:CompSeq b₁) .Lifespan() ) + 1 = card (b₁ .reachableFrom (choose (the_Vertices_of b₁))) )

proof end;

Lemma51: for b₁ being finite real-weighted WGraph
for b₂ being Nat
for b₃ being inducedSubgraph of b₁,((PRIM:CompSeq b₁) .-> b₂) .labeledV() ,((PRIM:CompSeq b₁) .-> b₂) .labeledE() holds b₃ is Tree-like

proof end;

Lemma52: for b₁ being finite connected real-weighted WGraph holds (PRIM:MST b₁) .labeledV() = the_Vertices_of b₁

proof end;

registration

let c₁ be finite connected real-weighted WGraph;
cluster spanning Tree-like Subgraph of a₁;
existence

proof end;

end;

definition

let c₁ be finite connected real-weighted WGraph;
let c₂ be spanning Tree-like WSubgraph of c₁;
attr a₂ is min-cost means :Def17: :: GLIB_004:def 17
for b₁ being spanning Tree-like WSubgraph of a₁ holds a₂ .cost() <= b₁ .cost() ;

end;

:: deftheorem Def17 defines min-cost GLIB_004:def 17 :

registration

let c₁ be finite connected real-weighted WGraph;
cluster spanning Tree-like min-cost Subgraph of a₁;
existence

proof end;

end;

definition

let c₁ be finite connected real-weighted WGraph;
mode minimumSpanningTree of a₁ is spanning Tree-like min-cost WSubgraph of a₁;

end;

theorem Th35: :: GLIB_004:35

for b₁, b₂ being finite connected real-weighted WGraph
for b₃ being WSubgraph of b₁ st b₃ is minimumSpanningTree of b₁ & b₁ == b₂ & the_Weight_of b₁ = the_Weight_of b₂ holds
b₃ is minimumSpanningTree of b₂

proof end;

theorem Th36: :: GLIB_004:36

for b₁ being finite connected real-weighted WGraph
for b₂ being minimumSpanningTree of b₁
for b₃ being WGraph st b₂ == b₃ & the_Weight_of b₂ = the_Weight_of b₃ holds
b₃ is minimumSpanningTree of b₁

proof end;

theorem Th37: :: GLIB_004:37

for b₁ being real-weighted WGraph holds
( b₁ == PRIM:Init b₁ & the_Weight_of b₁ = the_Weight_of (PRIM:Init b₁) & the_ELabel_of (PRIM:Init b₁) = {} & the_VLabel_of (PRIM:Init b₁) = (choose (the_Vertices_of b₁)) .--> 1 ) by Lemma38;

theorem Th38: :: GLIB_004:38

for b₁ being real-weighted WGraph holds
( (PRIM:Init b₁) .labeledV() = {(choose (the_Vertices_of b₁))} & (PRIM:Init b₁) .labeledE() = {} ) by Lemma39;

theorem Th39: :: GLIB_004:39

for b₁ being real-WEV WEVGraph st PRIM:NextBestEdges b₁ <> {} holds
ex b₂ being Vertex of b₁ st
( not b₂ in b₁ .labeledV() & PRIM:Step b₁ = (b₁ .labelEdge (choose (PRIM:NextBestEdges b₁)),1) .labelVertex b₂,1 ) by Lemma40;

theorem Th40: :: GLIB_004:40

for b₁ being real-WEV WEVGraph holds
( b₁ == PRIM:Step b₁ & the_Weight_of b₁ = the_Weight_of (PRIM:Step b₁) & b₁ .labeledE() c= (PRIM:Step b₁) .labeledE() & b₁ .labeledV() c= (PRIM:Step b₁) .labeledV() ) by Lemma41;

theorem Th41: :: GLIB_004:41

for b₁ being finite real-weighted WGraph
for b₂ being Nat holds
( b₁ == (PRIM:CompSeq b₁) .-> b₂ & the_Weight_of ((PRIM:CompSeq b₁) .-> b₂) = the_Weight_of b₁ ) by Lemma42;

theorem Th42: :: GLIB_004:42

for b₁ being finite real-weighted WGraph
for b₂ being Nat holds
( ((PRIM:CompSeq b₁) .-> b₂) .labeledV() is non empty Subset of (the_Vertices_of b₁) & ((PRIM:CompSeq b₁) .-> b₂) .labeledE() c= b₁ .edgesBetween (((PRIM:CompSeq b₁) .-> b₂) .labeledV() ) ) by Lemma43;

theorem Th43: :: GLIB_004:43

for b₁ being finite real-weighted WGraph
for b₂ being Nat
for b₃ being inducedSubgraph of b₁,((PRIM:CompSeq b₁) .-> b₂) .labeledV() ,((PRIM:CompSeq b₁) .-> b₂) .labeledE() holds b₃ is connected ;

theorem Th44: :: GLIB_004:44

for b₁ being finite real-weighted WGraph
for b₂ being Nat
for b₃ being inducedSubgraph of b₁,(((PRIM:CompSeq b₁) .-> b₂) .labeledV() ) holds b₃ is connected ;

theorem Th45: :: GLIB_004:45

for b₁ being finite real-weighted WGraph
for b₂ being Nat holds ((PRIM:CompSeq b₁) .-> b₂) .labeledV() c= b₁ .reachableFrom (choose (the_Vertices_of b₁)) by Lemma46;

theorem Th46: :: GLIB_004:46

for b₁ being finite real-weighted WGraph
for b₂, b₃ being Nat st b₂ <= b₃ holds
( ((PRIM:CompSeq b₁) .-> b₂) .labeledV() c= ((PRIM:CompSeq b₁) .-> b₃) .labeledV() & ((PRIM:CompSeq b₁) .-> b₂) .labeledE() c= ((PRIM:CompSeq b₁) .-> b₃) .labeledE() ) by Lemma47;

theorem Th47: :: GLIB_004:47

for b₁ being finite real-weighted WGraph
for b₂ being Nat holds
( PRIM:NextBestEdges ((PRIM:CompSeq b₁) .-> b₂) = {} iff ((PRIM:CompSeq b₁) .-> b₂) .labeledV() = b₁ .reachableFrom (choose (the_Vertices_of b₁)) ) by Lemma48;

theorem Th48: :: GLIB_004:48

for b₁ being finite real-weighted WGraph
for b₂ being Nat holds card (((PRIM:CompSeq b₁) .-> b₂) .labeledV() ) = min (b₂ + 1),(card (b₁ .reachableFrom (choose (the_Vertices_of b₁)))) by Lemma49;

theorem Th49: :: GLIB_004:49

for b₁ being finite real-weighted WGraph holds
( PRIM:CompSeq b₁ is halting & ((PRIM:CompSeq b₁) .Lifespan() ) + 1 = card (b₁ .reachableFrom (choose (the_Vertices_of b₁))) ) by Lemma50;

theorem Th50: :: GLIB_004:50

theorem Th51: :: GLIB_004:51

for b₁ being finite connected real-weighted WGraph holds (PRIM:MST b₁) .labeledV() = the_Vertices_of b₁ by Lemma52;

theorem Th52: :: GLIB_004:52

for b₁ being finite connected real-weighted WGraph
for b₂ being Nat holds ((PRIM:CompSeq b₁) .-> b₂) .labeledE() c= (PRIM:MST b₁) .labeledE()

proof end;

theorem Th53: :: GLIB_004:53

for b₁ being finite connected real-weighted WGraph
for b₂ being inducedWSubgraph of b₁,(PRIM:MST b₁) .labeledV() ,(PRIM:MST b₁) .labeledE() holds b₂ is minimumSpanningTree of b₁

proof end;