:: Proof of Dijkstra's Shortest Path Algorithm & Prim's Minimum Spanning
:: Tree Algorithm
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, PRE_POLY,
TARSKI, CARD_1, UPROOTS, CARD_3, ARYTM_3, FINSEQ_1, NAT_1, XXREAL_0,
FINSET_1, SUBSET_1, FINSEQ_2, ARYTM_1, GLIB_003, TREES_1, GLIB_000,
GLIB_001, REAL_1, PBOOLE, ZFMISC_1, FUNCT_2, ABIAN, PARTFUN1, MCART_1,
GLIB_002, WAYBEL_0, RELAT_2, RCOMP_1, GRAPH_1, GLIB_004;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, XFAMILY, CARD_1,
ORDINAL1, NUMBERS, SUBSET_1, DOMAIN_1, MCART_1, XCMPLX_0, XXREAL_0,
XREAL_0, RELAT_1, RELSET_1, PARTFUN1, FUNCT_1, FINSEQ_1, FINSEQ_2,
PBOOLE, FUNCT_2, RVSUM_1, ABIAN, UPROOTS, FINSET_1, NAT_1, FUNCOP_1,
FUNCT_4, GLIB_000, GLIB_001, GLIB_002, GLIB_003, RFUNCT_3, PRE_POLY;
constructors DOMAIN_1, BINOP_2, FINSOP_1, RVSUM_1, GRAPH_2, RFUNCT_3, UPROOTS,
GLIB_002, GLIB_003, XXREAL_2, RELSET_1, XTUPLE_0, WSIERP_1, XFAMILY,
FINSEQ_6;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FRAENKEL, FUNCT_1,
ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, CARD_1, GLIB_000,
ABIAN, GLIB_001, GLIB_002, GLIB_003, VALUED_0, RELSET_1, PRE_POLY, INT_1,
FINSEQ_1, XTUPLE_0, FINSEQ_2;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI;
equalities GLIB_000, GLIB_003, RVSUM_1, FUNCOP_1, ORDINAL1;
expansions TARSKI, GLIB_000, GLIB_003;
theorems CARD_1, CARD_2, FUNCOP_1, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, GLIB_002,
GLIB_003, ABIAN, INT_1, JORDAN12, NAT_1, PARTFUN1, PBOOLE, RELAT_1,
RVSUM_1, TARSKI, TREES_1, UPROOTS, XBOOLE_0, XBOOLE_1, XREAL_0, ZFMISC_1,
XREAL_1, XXREAL_0, ORDINAL1, FINSOP_1, FUNCT_7, MCART_1, RELSET_1,
PRE_POLY;
schemes NAT_1, SUBSET_1, RECDEF_1, CQC_SIM1, PBOOLE, PRE_CIRC;
begin :: Preliminaries
Lm1: for F being Function, x,y being set holds dom(F+*(x.-->y)) = dom F \/ {x}
proof
let F be Function, x,y be set;
thus dom(F+*(x.-->y)) = dom F \/ dom(x.-->y) by FUNCT_4:def 1
.= dom F \/ {x};
end;
Lm2: for F being Function, x,y,z being set st z in dom (F+*(x.-->y)) & not z
in dom F holds x = z
proof
let F be Function, x,y,z be set such that
A1: z in dom (F+*(x.-->y)) and
A2: not z in dom F;
dom (x.-->y) = {x};
then z in dom F \/ {x} by A1,FUNCT_4:def 1;
then z in {x} by A2,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
theorem Th1:
for f, g being Function holds support (f +* g) c= support f \/ support g
proof
let f, g be Function;
let a be object;
assume a in support (f +* g);
then
A1: (f +* g).a <> 0 by PRE_POLY:def 7;
assume
A2: not a in support f \/ support g;
then not a in support f by XBOOLE_0:def 3;
then
A3: f.a = 0 by PRE_POLY:def 7;
not a in support g by A2,XBOOLE_0:def 3;
then
A4: g.a = 0 by PRE_POLY:def 7;
a in dom g or not a in dom g;
hence contradiction by A1,A3,A4,FUNCT_4:11,13;
end;
theorem Th2:
for f being Function, x, y being object holds
support (f +* (x.-->y)) c= support f \/ {x}
proof
let f be Function, x, y be object;
let a be object;
assume a in support (f +* (x.-->y));
then
A1: (f +* (x.-->y)).a <> 0 by PRE_POLY:def 7;
per cases;
suppose
a = x;
then a in {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
a <> x;
then (f +* (x.-->y)).a = f.a by FUNCT_4:83;
then a in support f by A1,PRE_POLY:def 7;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th3:
for A,B being set, b being Rbag of A, b1 being Rbag of B, b2
being Rbag of A\B st b = b1 +* b2 holds Sum b = Sum b1 + Sum b2
proof
let A, B be set, b be Rbag of A, b1 be Rbag of B, b2 be Rbag of A\B such
that
A1: b = b1 +* b2;
dom b = dom b1 \/ dom b2 by A1,FUNCT_4:def 1;
then dom b1 c= dom b by XBOOLE_1:7;
then B c= dom b by PARTFUN1:def 2;
then
A2: B c= A by PARTFUN1:def 2;
set B1 = (EmptyBag A) +* b1;
A3: dom B1 = (dom EmptyBag A) \/ dom b1 by FUNCT_4:def 1
.= A \/ dom b1 by PARTFUN1:def 2
.= A \/ B by PARTFUN1:def 2
.= A by A2,XBOOLE_1:12;
support B1 c= (support EmptyBag A) \/ support b1 by Th1;
then reconsider B1 as Rbag of A by A3,PARTFUN1:def 2,PRE_POLY:def 8
,RELAT_1:def 18;
set B2 = (EmptyBag A) +* b2;
A4: dom B2 = (dom EmptyBag A) \/ dom b2 by FUNCT_4:def 1
.= A \/ dom b2 by PARTFUN1:def 2
.= A \/ (A\B) by PARTFUN1:def 2
.= A by XBOOLE_1:12;
support B2 c= (support EmptyBag A) \/ support b2 by Th1;
then reconsider B2 as Rbag of A by A4,PARTFUN1:def 2,PRE_POLY:def 8
,RELAT_1:def 18;
A5: now
let x be object;
assume
A6: x in A;
A7: dom b1 = B by PARTFUN1:def 2;
A8: dom b2 = A\B by PARTFUN1:def 2;
per cases;
suppose
A9: x in B;
then
A10: B1.x = b1.x by A7,FUNCT_4:13;
A11: not x in dom b2 by A9,XBOOLE_0:def 5;
then B2.x = (EmptyBag A).x by FUNCT_4:11
.= 0 by PBOOLE:5;
hence b.x = B1.x + B2.x by A1,A11,A10,FUNCT_4:11
.= (B1 + B2).x by PRE_POLY:def 5;
end;
suppose
A12: not x in B;
then
A13: B1.x = (EmptyBag A).x by A7,FUNCT_4:11
.= 0 by PBOOLE:5;
A14: x in dom b2 by A6,A8,A12,XBOOLE_0:def 5;
then B2.x = b2.x by FUNCT_4:13;
hence b.x = B1.x + B2.x by A1,A13,A14,FUNCT_4:13
.= (B1 + B2).x by PRE_POLY:def 5;
end;
end;
consider F2 being FinSequence of REAL such that
A15: Sum B2 = Sum F2 and
A16: F2 = B2*canFS(support B2) by UPROOTS:def 3;
rng canFS(support B2) = support B2 & support B2 c= dom B2 by FUNCT_2:def 3
,PRE_POLY:37;
then
A17: dom F2 = dom canFS(support B2) by A16,RELAT_1:27;
consider F1 being FinSequence of REAL such that
A18: Sum B1 = Sum F1 and
A19: F1 = B1*canFS(support B1) by UPROOTS:def 3;
consider f1 being FinSequence of REAL such that
A20: Sum b1 = Sum f1 and
A21: f1 = b1*canFS(support b1) by UPROOTS:def 3;
A22: rng canFS(support b1) = support b1 & support b1 c= dom b1 by FUNCT_2:def 3
,PRE_POLY:37;
then
A23: dom f1 = dom canFS(support b1) by A21,RELAT_1:27;
A24: now
let x be object;
hereby
assume
A25: x in support b1;
then
A26: b1.x <> 0 by PRE_POLY:def 7;
support b1 c= dom b1 by PRE_POLY:37;
then B1.x = b1.x by A25,FUNCT_4:13;
hence x in support B1 by A26,PRE_POLY:def 7;
end;
assume
A27: x in support B1;
then
A28: B1.x <> 0 by PRE_POLY:def 7;
per cases;
suppose
not x in dom b1;
then B1.x = (EmptyBag A).x by FUNCT_4:11
.= 0 by PBOOLE:5;
hence x in support b1 by A27,PRE_POLY:def 7;
end;
suppose
x in dom b1;
then B1.x = b1.x by FUNCT_4:13;
hence x in support b1 by A28,PRE_POLY:def 7;
end;
end;
then
A29: support b1 = support B1 by TARSKI:2;
A30: now
let k be Nat such that
A31: k in dom f1;
A32: (canFS(support b1)).k in rng canFS(support b1) by A23,A31,FUNCT_1:3;
thus f1.k = b1.((canFS(support b1)).k) by A21,A23,A31,FUNCT_1:13
.= B1.((canFS(support b1)).k) by A22,A32,FUNCT_4:13
.= F1.k by A19,A23,A29,A31,FUNCT_1:13;
end;
rng canFS(support B1) = support B1 & support B1 c= dom B1 by FUNCT_2:def 3
,PRE_POLY:37;
then dom F1 = dom canFS(support B1) by A19,RELAT_1:27;
then dom f1 = dom F1 by A23,A24,TARSKI:2;
then
A33: Sum B1 = Sum b1 by A20,A18,A30,FINSEQ_1:13;
consider f2 being FinSequence of REAL such that
A34: Sum b2 = Sum f2 and
A35: f2 = b2*canFS(support b2) by UPROOTS:def 3;
A36: rng canFS(support b2) = support b2 & support b2 c= dom b2 by FUNCT_2:def 3
,PRE_POLY:37;
then
A37: dom f2 = dom canFS(support b2) by A35,RELAT_1:27;
now
let x be object;
hereby
assume
A38: x in support b2;
then
A39: b2.x <> 0 by PRE_POLY:def 7;
support b2 c= dom b2 by PRE_POLY:37;
then B2.x = b2.x by A38,FUNCT_4:13;
hence x in support B2 by A39,PRE_POLY:def 7;
end;
assume
A40: x in support B2;
then
A41: B2.x <> 0 by PRE_POLY:def 7;
per cases;
suppose
not x in dom b2;
then B2.x = (EmptyBag A).x by FUNCT_4:11
.= 0 by PBOOLE:5;
hence x in support b2 by A40,PRE_POLY:def 7;
end;
suppose
x in dom b2;
then B2.x = b2.x by FUNCT_4:13;
hence x in support b2 by A41,PRE_POLY:def 7;
end;
end;
then
A42: support b2 = support B2 by TARSKI:2;
now
let k be Nat such that
A43: k in dom f2;
A44: (canFS(support b2)).k in rng canFS(support b2) by A37,A43,FUNCT_1:3;
thus f2.k = b2.((canFS(support b2)).k) by A35,A37,A43,FUNCT_1:13
.= B2.((canFS(support b2)).k) by A36,A44,FUNCT_4:13
.= F2.k by A16,A37,A42,A43,FUNCT_1:13;
end;
then Sum B2 = Sum b2 by A34,A35,A15,A36,A17,A42,FINSEQ_1:13,RELAT_1:27;
hence thesis by A33,A5,PBOOLE:3,UPROOTS:15;
end;
theorem Th4:
for X,x being set, b being Rbag of X st dom b = {x} holds Sum b = b.x
proof
let X,x be set, b be Rbag of X;
assume
A1: dom b = {x};
then
A2: x in dom b by TARSKI:def 1;
support b c= {x} & {x} c= X by A1,PRE_POLY:37;
then consider f being FinSequence of REAL such that
A3: f = b*canFS({x}) and
A4: Sum b = Sum f by UPROOTS:14;
reconsider bx = b.x as Element of REAL by XREAL_0:def 1;
f = b*<*x*> by A3,FINSEQ_1:94;
then f = <*bx*> by A2,FINSEQ_2:34;
hence thesis by A4,FINSOP_1:11;
end;
theorem Th5:
for A being set, 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
let A be set, b1,b2 be Rbag of A such that
A1: for x being set st x in A holds b1.x <= b2.x;
set S = support b1 \/ support b2;
A2: dom b2 = A by PARTFUN1:def 2;
then
A3: support b2 c= A by PRE_POLY:37;
A4: dom b1 = A by PARTFUN1:def 2;
then support b1 c= A by PRE_POLY:37;
then reconsider S as finite Subset of A by A3,XBOOLE_1:8;
consider f1 being FinSequence of REAL such that
A5: f1 = b1*canFS(S) and
A6: Sum b1 = Sum f1 by UPROOTS:14,XBOOLE_1:7;
consider f2 being FinSequence of REAL such that
A7: f2 = b2*canFS(S) and
A8: Sum b2 = Sum f2 by UPROOTS:14,XBOOLE_1:7;
A9: rng canFS(S) = S by FUNCT_2:def 3;
then
A10: dom f1 = dom canFS(S) by A4,A5,RELAT_1:27;
A11: now
let j be Nat;
assume j in Seg len f1;
then
A12: j in dom f1 by FINSEQ_1:def 3;
then
A13: (canFS(S)).j in S by A9,A10,FUNCT_1:3;
f1.j = b1.((canFS(S)).j) & f2.j = b2.((canFS(S)).j) by A5,A7,A10,A12,
FUNCT_1:13;
hence f1.j <= f2.j by A1,A13;
end;
dom f2 = dom canFS(S) by A2,A7,A9,RELAT_1:27;
then
A14: len f1 = len f2 by A10,FINSEQ_3:29;
f1 is Element of (len f1)-tuples_on REAL & f2 is Element of (len f2)
-tuples_on REAL by FINSEQ_2:92;
hence thesis by A6,A8,A14,A11,RVSUM_1:82;
end;
theorem
for A being set, 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
let A be set, b1,b2 be Rbag of A;
assume
A1: for x being set st x in A holds b1.x = b2.x;
then for x being set st x in A holds b2.x <= b1.x;
then
A2: Sum b2 <= Sum b1 by Th5;
for x being set st x in A holds b1.x <= b2.x by A1;
then Sum b1 <= Sum b2 by Th5;
hence thesis by A2,XXREAL_0:1;
end;
theorem
for A1,A2 being set, b1 being Rbag of A1, b2 being Rbag of A2 st b1 =
b2 holds Sum b1 = Sum b2
proof
let A1,A2 be set, b1 be Rbag of A1, b2 be Rbag of A2;
assume b1 = b2;
then ex f1 being FinSequence of REAL st Sum b1 = Sum f1 & f1 = b2*canFS(
support b2) by UPROOTS:def 3;
hence thesis by UPROOTS:def 3;
end;
theorem Th8:
for X, x being set, b being Rbag of X, y being Real st b =
(EmptyBag X) +* (x.-->y) holds Sum b = y
proof
let X, x be set, b be Rbag of X, y be Real such that
A1: b = (EmptyBag X) +* (x.-->y);
dom (x.-->y) = {x} & dom b = dom EmptyBag X \/ dom (x.-->y)
by A1,FUNCT_4:def 1;
then
A2: {x} c= dom b by XBOOLE_1:7;
then reconsider S = {x} as finite Subset of X by PARTFUN1:def 2;
support b c= S
proof
let a be object;
assume a in support b;
then
A3: b.a <> 0 by PRE_POLY:def 7;
assume not a in S;
then a <> x by TARSKI:def 1;
then b.a = (EmptyBag X).a by A1,FUNCT_4:83;
hence contradiction by A3,PBOOLE:5;
end;
then consider f being FinSequence of REAL such that
A4: f = b*canFS(S) and
A5: Sum b = Sum f by UPROOTS:14;
reconsider bx = b.x as Element of REAL by XREAL_0:def 1;
{x} c= X by A2,PARTFUN1:def 2;
then x in X by ZFMISC_1:31;
then canFS(S) = <*x*> & x in dom b by FINSEQ_1:94,PARTFUN1:def 2;
then f = <*bx*> by A4,FINSEQ_2:34;
hence Sum b = b.x by A5,FINSOP_1:11
.= y by A1,FUNCT_7:94;
end;
theorem
for X, x being set, b1, b2 being Rbag of X, y being Real st b2
= b1 +* (x.-->y) holds Sum b2 = Sum b1 + y - b1.x
proof
let X, x be set, b1, b2 be Rbag of X, y be Real such that
A1: b2 = b1 +* (x.-->y);
dom (x.-->y) = {x} & dom b2 = dom b1 \/ dom (x.-->y) by A1,FUNCT_4:def 1;
then {x} c= dom b2 by XBOOLE_1:7;
then {x} c= X by PARTFUN1:def 2;
then
A2: x in X by ZFMISC_1:31;
set c = (EmptyBag X) +* (x.-->y);
A3: dom c = (dom EmptyBag X) \/ dom (x.-->y) by FUNCT_4:def 1
.= X \/ dom (x.-->y) by PARTFUN1:def 2
.= X \/ {x}
.= X by A2,ZFMISC_1:40;
set a = b1 +* (x.-->0);
A4: dom a = dom b1 \/ dom (x.-->0) by FUNCT_4:def 1
.= X \/ dom (x.-->0) by PARTFUN1:def 2
.= X \/ {x}
.= X by A2,ZFMISC_1:40;
set b = (EmptyBag X) +* (x .--> b1.x);
A5: dom b = (dom EmptyBag X) \/ dom (x.-->b1.x) by FUNCT_4:def 1
.= X \/ dom (x.-->b1.x) by PARTFUN1:def 2
.= X \/ {x}
.= X by A2,ZFMISC_1:40;
support b c= (support EmptyBag X) \/ {x} by Th2;
then reconsider b as Rbag of X by A5,PARTFUN1:def 2,PRE_POLY:def 8
,RELAT_1:def 18;
support a c= support b1 \/ {x} by Th2;
then reconsider a as Rbag of X by A4,PARTFUN1:def 2,PRE_POLY:def 8
,RELAT_1:def 18;
support c c= (support EmptyBag X) \/ {x} by Th2;
then reconsider c as Rbag of X by A3,PARTFUN1:def 2,PRE_POLY:def 8
,RELAT_1:def 18;
now
let i be object;
assume i in X;
A6: (EmptyBag X).i = 0 by PBOOLE:5;
per cases;
suppose
A7: i = x;
thus (a+b).i = a.i + b.i by PRE_POLY:def 5
.= 0 qua Nat + b.i by A7,FUNCT_7:94
.= b1.i by A7,FUNCT_7:94;
end;
suppose
A8: i <> x;
thus (a+b).i = a.i + b.i by PRE_POLY:def 5
.= b1.i + b.i by A8,FUNCT_4:83
.= b1.i + (0 qua Nat) by A6,A8,FUNCT_4:83
.= b1.i;
end;
end;
then
A9: Sum b1 - Sum b = Sum a + Sum b - Sum b by PBOOLE:3,UPROOTS:15;
A10: Sum c = y & Sum b = b1.x by Th8;
now
let i be object;
assume i in X;
A11: (EmptyBag X).i = 0 by PBOOLE:5;
per cases;
suppose
A12: i = x;
hence b2.i = y by A1,FUNCT_7:94
.= 0 qua Nat+ c.i by A12,FUNCT_7:94
.= a.i + c.i by A12,FUNCT_7:94
.= (a+c).i by PRE_POLY:def 5;
end;
suppose
A13: i <> x;
then
A14: c.i = 0 by A11,FUNCT_4:83;
thus b2.i = b1.i by A1,A13,FUNCT_4:83
.= a.i + c.i by A13,A14,FUNCT_4:83
.= (a+c).i by PRE_POLY:def 5;
end;
end;
hence Sum b2 = Sum b1 - Sum b + Sum c by A9,PBOOLE:3,UPROOTS:15
.= Sum b1 + y - b1.x by A10;
end;
begin :: Graph preliminaries
definition
let G1 be real-weighted WGraph, G2 be WSubgraph of G1, v be set;
pred G2 is_mincost_DTree_rooted_at v means
G2 is Tree-like & for x
being Vertex of G2 holds 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;
definition
let G be real-weighted WGraph, W be DPath of G, x,y be set;
pred W is_mincost_DPath_from x,y means
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;
definition
let G be _finite real-weighted WGraph, x,y be set;
func G.min_DPath_cost(x,y) -> Real means
:Def3:
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
proof
set X = {W where W is DPath of G: W is_Walk_from x,y};
now
let e be object;
assume e in X;
then ex W being DPath of G st e = W & W is_Walk_from x,y;
then e in the set of all w where w is DPath of G;
hence e in G.allDPaths() by GLIB_001:def 38;
end;
then reconsider X as finite Subset of G.allDPaths() by TARSKI:def 3;
hereby
assume ex W being DWalk of G st W is_Walk_from x,y;
then consider W being DWalk of G such that
A1: W is_Walk_from x,y;
set P = the DPath of W;
P is_Walk_from x,y by A1,GLIB_001:160;
then P in X;
then reconsider X as non empty finite Subset of G .allDPaths();
deffunc F(Element of X) = $1.cost();
consider W1 being Element of X such that
A2: for W2 being Element of X holds F(W1) <= F(W2) from PRE_CIRC:sch 5;
W1 in X;
then consider WA being DPath of G such that
A3: WA = W1 and
A4: WA is_Walk_from x,y;
A5: now
let WB be DPath of G;
assume WB is_Walk_from x,y;
then WB in X;
then reconsider WB9 = WB as Element of X;
F(W1) <= F(WB9) by A2;
hence WA.cost() <= WB.cost() by A3;
end;
reconsider WA as DPath of G;
set IT = WA.cost();
take IT, WA;
thus WA is_mincost_DPath_from x,y by A4,A5;
thus IT = WA.cost();
end;
thus thesis;
end;
uniqueness
proof
let IT1,IT2 be Real;
hereby
assume ex W being DWalk of G st W is_Walk_from x,y;
given W1 being DPath of G such that
A6: W1 is_mincost_DPath_from x,y and
A7: IT1 = W1.cost();
given W2 being DPath of G such that
A8: W2 is_mincost_DPath_from x,y and
A9: IT2 = W2.cost();
W2 is_Walk_from x,y by A8;
then
A10: IT1 <= IT2 by A6,A7,A9;
W1 is_Walk_from x,y by A6;
then IT2 <= IT1 by A7,A8,A9;
hence IT1 = IT2 by A10,XXREAL_0:1;
end;
thus thesis;
end;
consistency;
end;
definition
func WGraphSelectors -> non empty finite Subset of NAT equals
{
VertexSelector, EdgeSelector, SourceSelector, TargetSelector, WeightSelector};
coherence;
end;
Lm3: for G being WGraph holds WGraphSelectors c= dom G
proof
let G be WGraph;
let x be object;
assume x in WGraphSelectors;
then x = VertexSelector or x = EdgeSelector or x = SourceSelector or x =
TargetSelector or x = WeightSelector by ENUMSET1:def 3;
hence x in dom G by GLIB_000:def 10,GLIB_003:def 4;
end;
registration
let G be WGraph;
cluster G|(WGraphSelectors) -> [Graph-like] [Weighted];
coherence
proof
set G2 = G|(WGraphSelectors);
A1: VertexSelector in WGraphSelectors by ENUMSET1:def 3;
A2: TargetSelector in WGraphSelectors by ENUMSET1:def 3;
then
A3: the_Target_of G2 = the_Target_of G by FUNCT_1:49;
A4: SourceSelector in WGraphSelectors by ENUMSET1:def 3;
then
A5: the_Source_of G2 = the_Source_of G by FUNCT_1:49;
A6: EdgeSelector in WGraphSelectors by ENUMSET1:def 3;
then
A7: the_Edges_of G2 = the_Edges_of G by FUNCT_1:49;
A8: dom G2 = dom G /\ WGraphSelectors by RELAT_1:61
.= WGraphSelectors by Lm3,XBOOLE_1:28;
then for x being object st x in _GraphSelectors holds x in dom G2
by A1,A6,A4
,A2,ENUMSET1:def 2;
then
A9: _GraphSelectors c= dom G2;
the_Vertices_of G2 = the_Vertices_of G by A1,FUNCT_1:49;
hence G2 is [Graph-like] by A7,A5,A3,A9,GLIB_000:5;
A10: WeightSelector in WGraphSelectors by ENUMSET1:def 3;
then G2.WeightSelector = G.WeightSelector by FUNCT_1:49;
then G2.WeightSelector is ManySortedSet of the_Edges_of G2 by A7,
GLIB_003:def 4;
hence thesis by A8,A10;
end;
end;
Lm4: for G being WGraph holds G == (G|(WGraphSelectors)) & the_Weight_of
G = the_Weight_of (G|(WGraphSelectors))
proof
let G be WGraph;
set G2 = G|(WGraphSelectors);
EdgeSelector in WGraphSelectors by ENUMSET1:def 3;
then
A1: the_Edges_of G2 = the_Edges_of G by FUNCT_1:49;
SourceSelector in WGraphSelectors by ENUMSET1:def 3;
then
A2: the_Source_of G2 = the_Source_of G by FUNCT_1:49;
TargetSelector in WGraphSelectors by ENUMSET1:def 3;
then
A3: the_Target_of G2 = the_Target_of G by FUNCT_1:49;
VertexSelector in WGraphSelectors by ENUMSET1:def 3;
then the_Vertices_of G2 = the_Vertices_of G by FUNCT_1:49;
hence G == G2 by A1,A2,A3;
WeightSelector in WGraphSelectors by ENUMSET1:def 3;
hence thesis by FUNCT_1:49;
end;
Lm5: for G being WGraph holds dom (G|(WGraphSelectors)) = WGraphSelectors
proof
let G be WGraph;
WGraphSelectors c= dom G by Lm3;
hence thesis by RELAT_1:62;
end;
definition
let G be WGraph;
func G.allWSubgraphs() -> non empty set means
:Def5:
for x being set holds x
in it iff ex G2 being WSubgraph of G st x = G2 & dom G2 = WGraphSelectors;
existence
proof
set G9 = G|(WGraphSelectors);
A1: G == G9 by Lm4;
A2: the_Weight_of G = the_Weight_of G9 by Lm4;
reconsider G9 as [Weighted] Subgraph of G by A1,GLIB_000:87;
the_Weight_of G9 = (the_Weight_of G) | the_Edges_of G9 by A2;
then reconsider G9 as WSubgraph of G by GLIB_003:def 10;
set Z = {bool the_Vertices_of G, bool the_Edges_of G, bool the_Source_of G
, bool the_Target_of G, bool the_Weight_of G};
set Y = union Z;
set X = Funcs(WGraphSelectors, Y);
defpred P[set] means $1 is WSubgraph of G;
consider IT being Subset of X such that
A3: for x being set holds x in IT iff x in X & P[x] from SUBSET_1:sch
1;
A4: now
let G2 be WSubgraph of G;
assume
A5: dom G2 = WGraphSelectors;
now
let y be object;
assume y in rng G2;
then consider x being object such that
A6: x in WGraphSelectors and
A7: G2.x = y by A5,FUNCT_1:def 3;
now
per cases by A6,ENUMSET1:def 3;
suppose
A8: x = VertexSelector;
A9: bool the_Vertices_of G in Z by ENUMSET1:def 3;
y = the_Vertices_of G2 by A7,A8;
hence y in Y by A9,TARSKI:def 4;
end;
suppose
A10: x = EdgeSelector;
A11: bool the_Edges_of G in Z by ENUMSET1:def 3;
y = the_Edges_of G2 by A7,A10;
hence y in Y by A11,TARSKI:def 4;
end;
suppose
x = SourceSelector;
then y = the_Source_of G2 by A7;
then y = (the_Source_of G) | the_Edges_of G2 by GLIB_000:45;
then
A12: G2.x c= the_Source_of G by RELAT_1:59,A7;
bool the_Source_of G in Z by ENUMSET1:def 3;
hence y in Y by A12,TARSKI:def 4,A7;
end;
suppose
x = TargetSelector;
then y = the_Target_of G2 by A7;
then y = (the_Target_of G) | the_Edges_of G2 by GLIB_000:45;
then
A13: G2.x c= the_Target_of G by RELAT_1:59,A7;
bool the_Target_of G in Z by ENUMSET1:def 3;
hence y in Y by A13,TARSKI:def 4,A7;
end;
suppose
x = WeightSelector;
then y = the_Weight_of G2 by A7;
then y = (the_Weight_of G) | the_Edges_of G2 by GLIB_003:def 10;
then
A14: G2.x c= the_Weight_of G by RELAT_1:59,A7;
bool the_Weight_of G in Z by ENUMSET1:def 3;
hence y in Y by A14,TARSKI:def 4,A7;
end;
end;
hence y in Y;
end;
hence rng G2 c= Y;
end;
A15: dom G9 = WGraphSelectors by Lm5;
then rng G9 c= Y by A4;
then G9 in X by A15,FUNCT_2:def 2;
then reconsider IT as non empty set by A3;
take IT;
let x be set;
hereby
assume
A16: x in IT;
then reconsider x9 = x as WSubgraph of G by A3;
take x9;
thus x9 = x;
ex f being Function st f = x & dom f = WGraphSelectors & rng f c= Y
by A16,FUNCT_2:def 2;
hence dom x9 = WGraphSelectors;
end;
given G2 being WSubgraph of G such that
A17: G2 = x and
A18: dom G2 = WGraphSelectors;
rng G2 c= Y by A4,A18;
then x in X by A17,A18,FUNCT_2:def 2;
hence thesis by A3,A17;
end;
uniqueness
proof
let IT1,IT2 be non empty set such that
A19: for x being set holds x in IT1 iff ex G2 being WSubgraph of G st
x = G2 & dom G2 = WGraphSelectors and
A20: for x being set holds x in IT2 iff ex G2 being WSubgraph of G st
x = G2 & dom G2 = WGraphSelectors;
now
let x be object;
x in IT1 iff ex G2 being WSubgraph of G st x = G2 & dom G2 =
WGraphSelectors by A19;
hence x in IT1 iff x in IT2 by A20;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let G be _finite WGraph;
cluster G.allWSubgraphs() -> finite;
coherence
proof
set Z = {bool the_Vertices_of G, bool the_Edges_of G, bool the_Source_of G
, bool the_Target_of G, bool the_Weight_of G}, Y = union Z;
for x being set st x in Z holds x is finite by ENUMSET1:def 3;
then reconsider Y as finite set by FINSET_1:7;
set X = Funcs(WGraphSelectors, Y);
now
let x be object;
assume x in G.allWSubgraphs();
then consider G2 being WSubgraph of G such that
A1: x = G2 and
A2: dom G2 = WGraphSelectors by Def5;
now
let y be object;
assume y in rng G2;
then consider x being object such that
A3: x in WGraphSelectors and
A4: G2.x = y by A2,FUNCT_1:def 3;
now
per cases by A3,ENUMSET1:def 3;
suppose
A5: x = VertexSelector;
A6: bool the_Vertices_of G in Z by ENUMSET1:def 3;
y = the_Vertices_of G2 by A4,A5;
hence y in Y by A6,TARSKI:def 4;
end;
suppose
A7: x = EdgeSelector;
A8: bool the_Edges_of G in Z by ENUMSET1:def 3;
y = the_Edges_of G2 by A4,A7;
hence y in Y by A8,TARSKI:def 4;
end;
suppose
x = SourceSelector;
then y = the_Source_of G2 by A4;
then y = (the_Source_of G) | the_Edges_of G2 by GLIB_000:45;
then
A9: G2.x c= the_Source_of G by RELAT_1:59,A4;
bool the_Source_of G in Z by ENUMSET1:def 3;
hence y in Y by A9,TARSKI:def 4,A4;
end;
suppose
x = TargetSelector;
then y = the_Target_of G2 by A4;
then y = (the_Target_of G) | the_Edges_of G2 by GLIB_000:45;
then
A10: G2.x c= the_Target_of G by RELAT_1:59,A4;
bool the_Target_of G in Z by ENUMSET1:def 3;
hence y in Y by A10,TARSKI:def 4,A4;
end;
suppose
x = WeightSelector;
then y = the_Weight_of G2 by A4;
then y = (the_Weight_of G) | the_Edges_of G2 by GLIB_003:def 10;
then
A11: G2.x c= the_Weight_of G by RELAT_1:59,A4;
bool the_Weight_of G in Z by ENUMSET1:def 3;
hence y in Y by A11,TARSKI:def 4,A4;
end;
end;
hence y in Y;
end;
then rng G2 c= Y;
hence x in X by A1,A2,FUNCT_2:def 2;
end;
then G.allWSubgraphs() c= X;
hence thesis;
end;
end;
definition
let G be WGraph, X be non empty Subset of G.allWSubgraphs();
redefine mode Element of X -> WSubgraph of G; :: redefines Element (SUBSET_1, definition)
coherence
proof
let x be Element of X;
ex G2 being WSubgraph of G st G2 = x & dom G2 = WGraphSelectors by Def5;
hence thesis;
end;
end;
definition
let G be _finite real-weighted WGraph;
func G.cost() -> Real equals
Sum the_Weight_of G;
coherence;
end;
theorem Th10:
for G1 being _finite real-weighted WGraph, e being set, G2 being
weight-inheriting [Weighted] removeEdge of G1,e st e in the_Edges_of G1 holds
G1.cost() = G2.cost() + (the_Weight_of G1).e
proof
let G1 be _finite real-weighted WGraph, e be set, G2 be weight-inheriting
[Weighted] removeEdge of G1,e;
set EG1 = the_Edges_of G1, EG2 = the_Edges_of G2;
assume
A1: e in EG1;
A2: dom the_Weight_of G1 = EG1 by PARTFUN1:def 2;
set b2 = (e .--> (the_Weight_of G1).e);
A3: dom b2 = {e};
A4: EG2 = EG1 \ {e} by GLIB_000:51;
then EG1 \ EG2 = EG1 /\ {e} by XBOOLE_1:48
.= {e} by A1,ZFMISC_1:46;
then reconsider b2 as ManySortedSet of EG1 \ EG2;
reconsider b2 as Rbag of EG1 \ EG2;
A5: the_Weight_of G2 = (the_Weight_of G1) | (EG2) by GLIB_003:def 10;
A6: now
let x be object;
assume x in dom the_Weight_of G1;
then
A7: x in EG1;
now
per cases;
suppose
A8: x in {e};
then
A9: x = e by TARSKI:def 1;
hence (the_Weight_of G2 +* b2).x = b2.e by A3,A8,FUNCT_4:13
.= (the_Weight_of G1).x by A9,FUNCOP_1:72;
end;
suppose
not x in {e};
then
(the_Weight_of G2 +* b2).x = (the_Weight_of G2).x & x in EG1 \ {e
} by A3,A7,FUNCT_4:11,XBOOLE_0:def 5;
hence (the_Weight_of G2 +* b2).x = (the_Weight_of G1).x by A4,A5,
FUNCT_1:49;
end;
end;
hence (the_Weight_of G1).x = (the_Weight_of G2 +* b2).x;
end;
dom (the_Weight_of G2 +* b2) = dom the_Weight_of G2 \/ {e} by A3,
FUNCT_4:def 1
.= (EG1 \ {e}) \/ {e} by A4,PARTFUN1:def 2
.= EG1 \/ {e} by XBOOLE_1:39
.= EG1 by A1,ZFMISC_1:40;
hence G1.cost() = G2.cost() + Sum b2 by A2,A6,Th3,FUNCT_1:2
.= G2.cost() + b2.e by A3,Th4
.= G2.cost() + (the_Weight_of G1).e by FUNCOP_1:72;
end;
theorem Th11:
for G being _finite real-weighted WGraph, V1 being non empty
Subset of the_Vertices_of G, E1 being Subset of G.edgesBetween(V1), G1 being
inducedWSubgraph of G,V1,E1, e being set, 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
let G be _finite real-weighted WGraph, V1 be non empty Subset of
the_Vertices_of G, E1 be Subset of G.edgesBetween(V1), G1 be inducedWSubgraph
of G,V1,E1, e being set, G2 be inducedWSubgraph of G,V1,E1 \/ {e};
assume that
A1: not e in E1 and
A2: e in G.edgesBetween(V1);
{e} c= G.edgesBetween(V1) by A2,ZFMISC_1:31;
then (E1 \/ {e}) c= G.edgesBetween(V1) by XBOOLE_1:8;
then
A3: the_Edges_of G2 = E1 \/ {e} by GLIB_000:def 37;
then
A4: dom the_Weight_of G2 = E1 \/ {e} by PARTFUN1:def 2;
set W2 = (e .--> (the_Weight_of G).e);
A6: the_Edges_of G1 = E1 by GLIB_000:def 37;
then the_Edges_of G2 \ the_Edges_of G1 = {e} \ E1 by A3,XBOOLE_1:40
.= {e} by A1,ZFMISC_1:59;
then reconsider W2 as ManySortedSet of (the_Edges_of G2 \ the_Edges_of G1);
reconsider W2 as Rbag of (the_Edges_of G2 \ the_Edges_of G1);
A7: the_Weight_of G1 = (the_Weight_of G) | E1 by A6,GLIB_003:def 10;
A8: now
let x be object;
assume x in dom the_Weight_of G2;
then
A9: x in E1 \/ {e} by A3;
the_Weight_of G2 = (the_Weight_of G) | (E1 \/ {e}) by A3,GLIB_003:def 10;
then
A10: (the_Weight_of G2).x = (the_Weight_of G).x by A9,FUNCT_1:49;
now
per cases;
suppose
not x in dom W2;
then
((the_Weight_of G1)+*W2).x = (the_Weight_of G1).x & x in E1 by A9,
FUNCT_4:11,XBOOLE_0:def 3;
hence ((the_Weight_of G1)+*W2).x = (the_Weight_of G2).x by A7,A10,
FUNCT_1:49;
end;
suppose
A11: x in dom W2;
then
A12: x = e by TARSKI:def 1;
((the_Weight_of G1)+*W2).x = W2.x by A11,FUNCT_4:13
.= (the_Weight_of G).e by A12,FUNCOP_1:72;
hence ((the_Weight_of G1)+*W2).x = (the_Weight_of G2).x by A10,A11,
TARSKI:def 1;
end;
end;
hence (the_Weight_of G2).x = ((the_Weight_of G1) +* W2).x;
end;
dom W2 = {e};
then
A13: Sum W2 = W2.e by Th4
.= (the_Weight_of G).e by FUNCOP_1:72;
dom ((the_Weight_of G1) +* W2) = dom the_Weight_of G1 \/ dom W2 by
FUNCT_4:def 1
.= E1 \/ {e} by A6,PARTFUN1:def 2;
hence thesis by A4,A8,A13,Th3,FUNCT_1:2;
end;
theorem Th12:
for G being _finite nonnegative-weighted WGraph, W being DPath of
G, x,y being set, 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
let G be _finite nonnegative-weighted WGraph, W be DPath of G, x,y be set,
m,n be Element of NAT;
set WC = W.cut(m,n);
A1: WC is_Walk_from WC.first(),WC.last() by GLIB_001:def 23;
assume
A2: W is_mincost_DPath_from x,y;
then
A3: W is_Walk_from x,y;
then
A4: W.1 = x & W.(len W) = y by GLIB_001:17;
now
per cases;
suppose
A5: m is odd & n is odd & m <= n & n <= len W;
set W1 = W.cut(1,m), W3 = W.cut(n,len W);
A6: 1 <= n by A5,ABIAN:12;
then
A7: W.cut(1,n).append(W3) = W.cut(1,len W) by A5,GLIB_001:38,JORDAN12:2
.= W by GLIB_001:39;
W.cut(1,n).last() = W.n by A5,A6,GLIB_001:37,JORDAN12:2
.= W3.first() by A5,GLIB_001:37;
then
A8: W.cost() = W.cut(1,n).cost() + W3.cost() by A7,GLIB_003:24;
A9: 1 <= m by A5,ABIAN:12;
then
A10: W1.append(WC) = W.cut(1,n) by A5,GLIB_001:38,JORDAN12:2;
A11: m <= len W by A5,XXREAL_0:2;
then W1.last() = W.m by A5,A9,GLIB_001:37,JORDAN12:2
.= WC.first() by A5,GLIB_001:37;
then W.cut(1,n).cost() = W1.cost() + WC.cost() by A10,GLIB_003:24;
then
A12: W.cost() = WC.cost() + (W1.cost() + W3.cost()) by A8;
A13: W3 is_Walk_from W.n, W.(len W) by A5,GLIB_001:37;
A14: W1 is_Walk_from W.1, W.m by A5,A9,A11,GLIB_001:37,JORDAN12:2;
now
assume not WC is_mincost_DPath_from WC.first(),WC.last();
then consider W2 being DPath of G such that
A15: W2 is_Walk_from WC.first(), WC.last() and
A16: W2.cost() < WC.cost() by A1;
set WA = W1.append(W2), WB = WA.append(W3);
set WB2 = the DPath of WB;
A17: WC.last() = W.n by A5,GLIB_001:37;
A18: WC.first() = W.m by A5,GLIB_001:37;
then WA is_Walk_from W.1, W.n by A14,A15,A17,GLIB_001:31;
then WB is_Walk_from x,y by A4,A13,GLIB_001:31;
then
A19: WB2 is_Walk_from x,y by GLIB_001:160;
W2.first() = W.m by A15,A18,GLIB_001:def 23;
then
A20: W1.last() = W2.first() by A5,A9,A11,GLIB_001:37,JORDAN12:2;
then
A21: WA.cost() = W1.cost() + W2.cost() by GLIB_003:24;
W2.last() = W.n by A15,A17,GLIB_001:def 23;
then W3.first() = W2.last() by A5,GLIB_001:37
.= WA.last() by A20,GLIB_001:30;
then WB.cost() = W1.cost() + W2.cost() + W3.cost() by A21,GLIB_003:24
.= W2.cost() + (W1.cost() + W3.cost());
then
A22: WB.cost() < W.cost() by A12,A16,XREAL_1:8;
WB2.cost() <= WB.cost() by GLIB_003:30;
then WB2.cost() < W.cost() by A22,XXREAL_0:2;
hence contradiction by A2,A19;
end;
hence thesis;
end;
suppose
not (m is odd & n is odd & m <= n & n <= len W);
then
A23: WC = W by GLIB_001:def 11;
then WC.first() = x by A3,GLIB_001:def 23;
hence thesis by A2,A23,GLIB_001:def 23;
end;
end;
hence thesis;
end;
theorem
for G being _finite real-weighted WGraph, W1,W2 being DPath of G, 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
let G be _finite real-weighted WGraph, W1,W2 be DPath of G, x,y be set;
assume that
A1: W1 is_mincost_DPath_from x,y and
A2: W2 is_mincost_DPath_from x,y;
W2 is_Walk_from x,y by A2;
then
A3: W1.cost() <= W2.cost() by A1;
W1 is_Walk_from x,y by A1;
then W2.cost() <= W1.cost() by A2;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th14:
for G being _finite real-weighted WGraph, W being DPath of G, x,y
being set st W is_mincost_DPath_from x,y holds G.min_DPath_cost(x,y) = W.cost()
by Def3;
begin :: Definitions for Dijkstra's Shortest Path Algorithm
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;
definition
let X1,X3 be set, X2 be non empty set;
let x be Element of [: PFuncs(X1,X3),X2 :];
redefine func x`1 -> Element of PFuncs(X1,X3); :: redefines `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
end;
registration
let G be _finite _Graph, L be DIJK:Labeling of G;
cluster L`1 -> finite for set;
coherence
proof
dom L`1 c= the_Vertices_of G;
hence thesis by FINSET_1:10;
end;
cluster L`2 -> finite for set;
coherence;
end;
definition
let G be real-weighted WGraph, L be DIJK:Labeling of G;
func DIJK:NextBestEdges(L) -> Subset of the_Edges_of G means
:Def7:
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
proof
defpred P[set] means $1 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).$1)+(the_Weight_of G).$1 <= (L`1).((the_Source_of G).e2)
+(the_Weight_of G).e2;
consider IT being Subset of the_Edges_of G such that
A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
now
let e1 be set;
thus e1 in IT implies P[e1] by A1;
assume
A2: P[e1];
then e1 in the_Edges_of G by GLIB_000:def 16;
hence e1 in IT by A1,A2;
end;
hence thesis;
end;
uniqueness
proof
defpred P[set] means $1 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).$1)+(the_Weight_of G).$1 <= (L`1).((the_Source_of G).e2)
+(the_Weight_of G).e2;
let IT1,IT2 be Subset of the_Edges_of G such that
A3: for y being set holds y in IT1 iff P[y] and
A4: for y being set holds y in IT2 iff P[y];
now
let x be object;
reconsider xx=x as set by TARSKI:1;
hereby
assume x in IT1;
then P[xx] by A3;
hence x in IT2 by A4;
end;
assume x in IT2;
then P[xx] by A4;
hence x in IT1 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let G be real-weighted WGraph, L be DIJK:Labeling of G;
func DIJK:Step(L) -> DIJK:Labeling of G equals
:Def8:
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
proof
set V = the_Vertices_of G, E = the_Edges_of G;
set BE = DIJK:NextBestEdges(L), e = the Element of BE;
set nE = L`2 \/ {e};
set s = (the_Source_of G).e, t = (the_Target_of G).e;
set val = (L`1).s + (the_Weight_of G).e;
now
assume
A1: BE <> {};
then e in BE;
then reconsider e9 = e as Element of E;
A2: e in BE by A1;
then reconsider t9 = t as Element of V by FUNCT_2:5;
L`2 in bool E & {e9} c= E by A2,ZFMISC_1:31;
then
A3: nE c= E by XBOOLE_1:8;
{t9} c= V & dom (L`1+*(t .--> val)) = dom L`1 \/ {t} by Lm1;
then
A4: dom (L`1+*(t .--> val)) c= V by XBOOLE_1:8;
rng (L`1+*(t .--> val)) c= REAL;
then L`1+*(t .--> val) in PFuncs(V, REAL) by A4,PARTFUN1:def 3;
hence [ L`1+*(t .--> val), nE ] is DIJK:Labeling of G by A3,
ZFMISC_1:def 2;
end;
hence thesis;
end;
consistency;
end;
definition
let G be real-weighted WGraph, src be Vertex of G;
func DIJK:Init(src) -> DIJK:Labeling of G equals
[src .--> 0, {}];
coherence
proof
set f = src .--> 0;
dom f = {src} & rng f = {0} by FUNCOP_1:8;
then
A1: f in PFuncs(the_Vertices_of G, REAL) by PARTFUN1:def 3;
{} c= the_Edges_of G;
hence thesis by A1,ZFMISC_1:def 2;
end;
end;
definition
let G be real-weighted WGraph;
mode DIJK:LabelingSeq of G -> ManySortedSet of NAT means
:Def10:
for n being Nat holds it.n is DIJK:Labeling of G;
existence
proof
defpred P[object,object] means $2 is DIJK:Labeling of G;
:: !!! Funkcja stala ???
A1: now
let i be object;
assume i in NAT;
reconsider r = [{},{}] as object;
take r;
{} is PartFunc of the_Vertices_of G, REAL by RELSET_1:12;
then
A2: {} in PFuncs(the_Vertices_of G, REAL) by PARTFUN1:45;
{} c= the_Edges_of G;
hence P[i,r] by A2,ZFMISC_1:def 2;
end;
consider s being ManySortedSet of NAT such that
A3: for i being object st i in NAT holds P[i,s.i] from PBOOLE:sch 3(A1);
take s;
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
end;
definition
let G be real-weighted WGraph, S be DIJK:LabelingSeq of G, n be Nat;
redefine func S.n -> DIJK:Labeling of G; :: redefines . (FUNCT_1, definition)
coherence by Def10;
end;
definition
let G be real-weighted WGraph, src be Vertex of G;
func DIJK:CompSeq(src) -> DIJK:LabelingSeq of G means
:Def11:
it.0 = DIJK:Init(src) & for n being Nat holds it.(n+1) = DIJK:Step(it.n);
existence
proof
defpred P[set,set,set] means ($2 is DIJK:Labeling of G & ex Gn,Gn1 being
DIJK:Labeling of G st $2 = Gn & $3 = Gn1 & Gn1 = DIJK:Step(Gn)) or (not $2 is
DIJK:Labeling of G & $2 = $3);
now
let n be Nat, x be set;
now
per cases;
suppose
x is DIJK:Labeling of G;
then reconsider Gn=x as DIJK:Labeling of G;
P[n,x,DIJK:Step(Gn)];
hence ex y being set st P[n,x,y];
end;
suppose
not x is DIJK:Labeling of G;
hence ex y being set st P[n,x,y];
end;
end;
hence ex y being set st P[n,x,y];
end;
then
A1: for n being Nat for x being set ex y being set st P[n,x,y];
consider IT being Function such that
A2: dom IT = NAT & IT.0 = DIJK:Init(src) & for n being Nat
holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
reconsider IT as ManySortedSet of NAT by A2,PARTFUN1:def 2,RELAT_1:def 18;
defpred P2[Nat] means IT.$1 is DIJK:Labeling of G;
A3: now
let n be Nat;
assume
A4: P2[n];
ex Gn,Gn1 being DIJK:Labeling of G st IT.n = Gn & IT.(n+ 1) = Gn1 &
Gn1 = DIJK:Step(Gn) by A2,A4;
hence P2[n+1];
end;
A5: P2[ 0 ] by A2;
for n being Nat holds P2[n] from NAT_1:sch 2(A5,A3);
then reconsider IT as DIJK:LabelingSeq of G by Def10;
reconsider IT as DIJK:LabelingSeq of G;
take IT;
thus IT.0 = DIJK:Init(src) by A2;
let n be Nat;
reconsider n9= n as Element of NAT by ORDINAL1:def 12;
ex Gn,Gn1 being DIJK:Labeling of G st IT.n9 = Gn & IT.(n +1) = Gn1 &
Gn1 = DIJK:Step(Gn) by A2;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be DIJK:LabelingSeq of G such that
A6: IT1.0 = DIJK:Init(src) and
A7: for n being Nat holds IT1.(n+1) = DIJK:Step(IT1.n) and
A8: IT2.0 = DIJK:Init(src) and
A9: for n being Nat holds IT2.(n+1) = DIJK:Step(IT2.n);
defpred P[Nat] means IT1.$1 = IT2.$1;
now
let n be Nat;
assume P[n];
then IT1.(n+1) = DIJK:Step(IT2.n) by A7
.= IT2.(n+1) by A9;
hence P[n+1];
end;
then
A10: for n being Nat st P[n] holds P[n+1];
A11: P[ 0 ] by A6,A8;
for n being Nat holds P[n] from NAT_1:sch 2(A11,A10);
then for n being object st n in NAT holds IT1.n = IT2.n;
hence IT1 = IT2 by PBOOLE:3;
end;
end;
definition
let G be real-weighted WGraph, src be Vertex of G;
func DIJK:SSSP(G,src) -> DIJK:Labeling of G equals
DIJK:CompSeq(src)
.Result();
coherence
proof
set DCS = DIJK:CompSeq(src);
DCS.Result() = DCS.(DCS.Lifespan());
hence thesis;
end;
end;
begin :: Dijkstra's Algorithm Theorems
theorem Th15:
for G being _finite real-weighted WGraph, L be DIJK:Labeling of G
holds (card dom (DIJK:Step(L))`1 = card dom L`1 iff DIJK:NextBestEdges(L) = {})
& (card dom (DIJK:Step(L))`1 = card dom L`1 + 1 iff DIJK:NextBestEdges(L)<>{})
proof
let G be _finite real-weighted WGraph, L be DIJK:Labeling of G;
set BestEdges = DIJK:NextBestEdges(L), e = the Element of BestEdges;
set nextEG = L`2 \/ {e}, nL = DIJK:Step(L);
set src = (the_Source_of G).e, target = (the_Target_of G).e;
set val = (L`1).src + (the_Weight_of G).e;
hereby
assume
A1: card dom nL`1 = card dom L`1;
now
assume
A2: BestEdges <> {};
then nL = [L`1+*(target .--> val), nextEG] by Def8;
then nL`1 = L`1+*(target .--> val);
then
A3: dom nL`1 = dom L`1 \/ {target} by Lm1;
e in BestEdges by A2;
then reconsider target as Vertex of G by FUNCT_2:5;
e DSJoins dom L`1,the_Vertices_of G \ dom L`1, G by A2,Def7;
then target in the_Vertices_of G \ dom L`1;
then not target in dom L`1 by XBOOLE_0:def 5;
then card dom nL`1 = card dom L`1 + 1 by A3,CARD_2:41;
hence contradiction by A1;
end;
hence BestEdges = {};
end;
thus BestEdges = {} implies card dom nL`1 = card dom L`1 by Def8;
hereby
assume
A4: card dom nL`1 = card dom L`1 + 1;
now
assume BestEdges = {};
then 0 + card dom L`1 = card dom L`1 + 1 by A4,Def8;
hence contradiction;
end;
hence BestEdges <> {};
end;
assume
A5: BestEdges <> {};
then nL = [L`1+*(target .--> val), nextEG] by Def8;
then nL`1 = L`1+*(target .--> val);
then
A6: dom nL`1 = dom L`1 \/ {target} by Lm1;
e in BestEdges by A5;
then reconsider target as Vertex of G by FUNCT_2:5;
e DSJoins dom L`1,the_Vertices_of G \ dom L`1, G by A5,Def7;
then target in the_Vertices_of G \ dom L`1;
then not target in dom L`1 by XBOOLE_0:def 5;
hence thesis by A6,CARD_2:41;
end;
theorem Th16:
for G being real-weighted WGraph, L be DIJK:Labeling of G holds
dom L`1 c= dom (DIJK:Step(L))`1 & L`2 c= (DIJK:Step(L))`2
proof
let G be real-weighted WGraph, L be DIJK:Labeling of G;
set nL = DIJK:Step(L);
set BestEdges = DIJK:NextBestEdges(L), e = the Element of BestEdges;
set NextEG = L`2 \/ {e}, target = (the_Target_of G).e;
set val = (L`1).((the_Source_of G).e) + (the_Weight_of G).e;
now
per cases;
suppose
BestEdges = {};
hence thesis by Def8;
end;
suppose BestEdges <> {};
then
A1: nL = [L`1+*(target .--> val), NextEG] by Def8;
then nL`1 = L`1+*(target .--> val);
then
A2: dom nL`1 = dom L`1 \/ {target} by Lm1;
now
let x be object;
assume
A3: x in dom L`1;
dom L`1 c= dom nL`1 by A2,XBOOLE_1:7;
hence x in dom nL`1 by A3;
end;
hence dom L`1 c= dom nL`1;
now
let x be object;
assume
A4: x in L`2;
L`2 c= NextEG & NextEG = nL`2 by A1,XBOOLE_1:7;
hence x in nL`2 by A4;
end;
hence L`2 c= nL`2;
end;
end;
hence thesis;
end;
theorem
for G being real-weighted WGraph, src be Vertex of G holds
dom ((DIJK:Init(src))`1) = {src};
theorem Th18:
for G being real-weighted WGraph, src being Vertex of G, 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
let G be real-weighted WGraph, src be Vertex of G, i,j be Nat;
set DCS = DIJK:CompSeq(src);
set dDCS = dom (DCS.i)`1;
set eDCS = (DCS.i)`2;
defpred P[Nat] means dDCS c= dom (DCS.(i+$1))`1 & eDCS c= (DCS.(i+$1))`2;
assume i <= j;
then
A1: ex x being Nat st j = i + x by NAT_1:10;
now
let k be Nat;
DCS.(i+k+1) = DIJK:Step(DCS.(i+k)) by Def11;
then
A2: dom (DCS.(i+k))`1 c= dom (DCS.(i+k+1))`1 & (DCS.(i+k))`2 c= (DCS.(i+k+
1))`2 by Th16;
assume dDCS c= dom (DCS.(i+k))`1 & eDCS c= (DCS.(i+k))`2;
hence dDCS c= dom (DCS.(i+(k+1)))`1 & eDCS c= (DCS.(i+(k+1)))`2 by A2;
end;
then
A3: for k being Nat st P[k] holds P[k+1];
A4: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
hence thesis by A1;
end;
theorem Th19:
for G being _finite real-weighted WGraph, src being Vertex of G,
n being Nat holds dom (DIJK:CompSeq(src).n)`1 c= G.reachableDFrom(src)
proof
let G be _finite real-weighted WGraph, src be Vertex of G;
set DCS = DIJK:CompSeq(src);
defpred P[Nat] means dom (DCS.$1)`1 c= G.reachableDFrom(src);
DCS.0 = DIJK:Init(src) by Def11;
then
A1: dom (DCS.0)`1 = {src};
now
let k be Nat such that
A2: dom (DCS.k)`1 c= G.reachableDFrom(src);
set Gk = DCS.k, NextG = DCS.(k+1);
set BestEdges = DIJK:NextBestEdges(Gk), e = the Element of BestEdges;
set NextEG = Gk`2 \/ {e};
set v1 = (the_Source_of G).e, target = (the_Target_of G).e;
set pc = Gk`1.v1, ec = (the_Weight_of G).e;
A3: NextG = DIJK:Step(Gk) by Def11;
now
let x be object;
assume
A4: x in dom (DCS.(k+1))`1;
now
per cases;
suppose
BestEdges = {};
then Gk = NextG by A3,Def8;
hence x in G.reachableDFrom(src) by A2,A4;
end;
suppose
A5: BestEdges <> {};
set xx = x;
reconsider xx as Vertex of G by A4;
e DSJoins dom Gk`1,the_Vertices_of G \ dom Gk`1,G by A5,Def7;
then
A6: v1 in dom Gk`1;
then reconsider v19 = v1 as Vertex of G;
NextG = [Gk`1+*(target .--> (pc+ec)),NextEG] by A3,A5,Def8;
then
A7: NextG`1 = Gk`1+*(target .--> (pc+ec));
now
per cases;
suppose
xx in dom Gk`1;
hence xx in G.reachableDFrom(src) by A2;
end;
suppose
A8: not xx in dom Gk`1;
A9: e in BestEdges by A5;
(the_Target_of G). e = xx by A4,A7,A8,Lm2;
then e DJoins v19,xx,G by A9;
hence xx in G.reachableDFrom(src) by A2,A6,GLIB_002:19;
end;
end;
hence x in G.reachableDFrom(src);
end;
end;
hence x in G.reachableDFrom(src);
end;
hence dom (DCS.(k+1))`1 c= G.reachableDFrom(src);
end;
then
A10: for k being Nat st P[k] holds P[k+1];
src in G.reachableDFrom(src) by GLIB_002:18;
then
A11: P[ 0 ] by A1,ZFMISC_1:31;
for n being Nat holds P[n] from NAT_1:sch 2(A11,A10);
hence thesis;
end;
theorem Th20:
for G being _finite real-weighted WGraph, src being Vertex of G,
n being Nat holds DIJK:NextBestEdges(DIJK:CompSeq(src).n) = {} iff dom (
DIJK:CompSeq(src).n)`1 = G.reachableDFrom(src)
proof
let G be _finite real-weighted WGraph, src be Vertex of G, n be Nat;
set DCS = DIJK:CompSeq(src), RFS = G.reachableDFrom(src);
set Gn = DCS.n, Gn1a = DCS.(n+1);
set BestEdges = DIJK:NextBestEdges(Gn);
set SGn = the_Source_of G;
set TGn = the_Target_of G;
hereby
assume
A1: BestEdges = {};
now
defpred P[set] means SGn.$1 in dom Gn`1 & not TGn.$1 in dom Gn`1;
assume
A2: dom Gn`1 <> RFS;
consider BE1 being Subset of the_Edges_of G such that
A3: for x being set holds x in BE1 iff x in the_Edges_of G & P[x]
from SUBSET_1:sch 1;
dom Gn`1 c= RFS by Th19;
then
A4: dom Gn`1 c< RFS by A2,XBOOLE_0:def 8;
now
DCS.0 = DIJK:Init(src) by Def11;
then dom (DCS.0)`1 = {src};
then
A5: src in dom (DCS.0)`1 by TARSKI:def 1;
assume
A6: BE1 = {};
consider v being object such that
A7: v in RFS and
A8: not v in dom Gn`1 by A4,XBOOLE_0:6;
reconsider v as Vertex of G by A7;
consider W being directed Walk of G such that
A9: W is_Walk_from src, v by A7,GLIB_002:def 6;
defpred P[Nat] means $1 is odd & $1 <= len W & not (W.$1 in dom Gn`1);
W.(len W) = W.last() by GLIB_001:def 7
.= v by A9,GLIB_001:def 23;
then
A10: ex k being Nat st P[k] by A8;
consider k being Nat such that
A11: P[k] & for m being Nat st P[m] holds k <= m from NAT_1:sch 5(
A10);
A12: dom (DCS.0)`1 c= dom Gn`1 by Th18;
now
per cases;
suppose
k = 1;
then W.k = W.first() by GLIB_001:def 6
.= src by A9,GLIB_001:def 23;
hence contradiction by A5,A12,A11;
end;
suppose
A13: k <> 1;
reconsider k9=k as odd Element of NAT by A11,ORDINAL1:def 12;
1 <= k by A11,ABIAN:12;
then 1 < k by A13,XXREAL_0:1;
then 1+1 < k+1 by XREAL_1:8;
then 2*1 <= k by NAT_1:13;
then reconsider k2a = k9-2*1 as odd Element of NAT by INT_1:5;
set e = W.(k2a+1);
A14: k - 2 < len W - 0 by A11,XREAL_1:15;
then
A15: e DJoins W.k2a, W.(k2a+2), G by GLIB_001:122;
then
A16: (the_Target_of G).e = W.(k2a+2);
k2a < k - 0 by XREAL_1:15;
then
A17: W.(k2a) in dom Gn`1 by A11,A14;
e in the_Edges_of G & (the_Source_of G).e = W.k2a by A15;
hence contradiction by A3,A6,A11,A17,A16;
end;
end;
hence contradiction;
end;
then reconsider BE1 as non empty finite set;
deffunc F(Element of BE1) = (Gn`1).((the_Source_of G).$1) + (
the_Weight_of G).($1);
consider e1 being Element of BE1 such that
A18: for e2 being Element of BE1 holds F(e1) <= F(e2) from PRE_CIRC:sch 5;
A19: not (TGn).e1 in dom Gn`1 by A3;
A20: e1 in the_Edges_of G by A3;
then (TGn).e1 in the_Vertices_of G by FUNCT_2:5;
then
A21: (TGn).e1 in the_Vertices_of G \ dom Gn`1 by A19,XBOOLE_0:def 5;
A22: now
let y be set;
assume
A23: y DSJoins dom Gn`1, the_Vertices_of G \ dom Gn`1,G;
then (TGn).y in the_Vertices_of G \ dom Gn`1;
then
A24: not (TGn).y in dom Gn`1 by XBOOLE_0:def 5;
y in the_Edges_of G & (SGn).y in dom Gn`1 by A23;
then y in BE1 by A3,A24;
hence
(Gn`1).((the_Source_of G).e1) + (the_Weight_of G).e1 <= (Gn`1).((
the_Source_of G).y) + (the_Weight_of G).y by A18;
end;
(SGn).e1 in dom Gn`1 by A3;
then e1 DSJoins dom Gn`1, the_Vertices_of G \ dom Gn`1, G by A20,A21;
hence contradiction by A1,A22,Def7;
end;
hence dom (DCS.n)`1 = RFS;
end;
assume
A25: dom (DCS.n)`1 = RFS;
A26: Gn1a = DIJK:Step(Gn) by Def11;
now
assume BestEdges <> {};
then
A27: card dom Gn1a`1 = card RFS + 1 by A26,A25,Th15;
Segm card dom Gn1a`1 c= Segm card RFS by Th19,CARD_1:11;
then card RFS + 1 <= card RFS + 0 by A27,NAT_1:39;
hence contradiction by XREAL_1:6;
end;
hence thesis;
end;
theorem Th21:
for G being _finite real-weighted WGraph, s being Vertex of G, n
being Nat holds card dom (DIJK:CompSeq(s).n)`1 = min(n+1, card(G.reachableDFrom
(s)))
proof
let G be _finite real-weighted WGraph, src be Vertex of G;
set DCS = DIJK:CompSeq( src), VL0 = dom (DCS.0)`1;
set RFS = G.reachableDFrom(src);
defpred P[Nat] means card dom (DCS.$1)`1 = min($1+1, card RFS);
src in RFS by GLIB_002:18;
then {src} c= RFS by ZFMISC_1:31;
then card {src} <= card RFS by NAT_1:43;
then
A1: 0+1 <= card RFS by CARD_1:30;
now
let k be Nat such that
A2: card dom (DCS.k)`1 = min(k+1, card RFS);
set Gk = DCS.k, Gk1b = DCS.(k+1);
set BestEdges = DIJK:NextBestEdges(Gk);
A3: DCS.(k+1) = DIJK:Step(DCS.k) by Def11;
now
per cases;
suppose
A4: BestEdges = {};
then card dom Gk`1 = card RFS by Th20;
then card RFS <= k+1 by A2,XXREAL_0:def 9;
then
A5: card RFS <= k+1+1 by NAT_1:12;
card dom Gk1b`1 = card dom Gk`1 by A3,A4,Th15;
then card dom Gk1b`1 = card RFS by A4,Th20;
hence card dom Gk1b`1 = min((k+1)+1, card RFS) by A5,XXREAL_0:def 9;
end;
suppose
A6: BestEdges <> {};
then
A7: dom Gk`1 <> RFS by Th20;
A8: now
dom Gk`1 c= RFS by Th19;
then
A9: dom Gk`1 c< RFS by A7,XBOOLE_0:def 8;
assume card dom Gk`1 = card RFS;
hence contradiction by A9,CARD_2:48;
end;
then k+1 <= card RFS by A2,XXREAL_0:def 9;
then
A10: k+1+1 <= card RFS + 1 by XREAL_1:6;
k+1+1 <> card RFS + 1 by A2,A8;
then k+1+1 < card RFS + 1 by A10,XXREAL_0:1;
then
A11: (k+1+1) <= card RFS by NAT_1:13;
card dom Gk1b`1 = card dom Gk`1 + 1 by A3,A6,Th15;
then card dom Gk1b`1 = (k+1)+1 by A2,A8,XXREAL_0:15;
hence card dom Gk1b`1 = min((k+1)+1, card RFS) by A11,XXREAL_0:def 9;
end;
end;
hence card dom (DCS.(k+1))`1 = min((k+1)+1, card RFS);
end;
then
A12: for k being Nat st P[k] holds P[k+1];
DCS.0 = DIJK:Init(src) by Def11;
then card VL0 = card {src}
.= 1 by CARD_1:30;
then
A13: P[ 0 ] by A1,XXREAL_0:def 9;
for n being Nat holds P[n] from NAT_1:sch 2(A13,A12);
hence thesis;
end;
theorem Th22:
for G being _finite real-weighted WGraph, src being Vertex of G,
n being Nat holds (DIJK:CompSeq(src).n)`2 c= G.edgesBetween(dom (DIJK:CompSeq(
src).n)`1)
proof
let G be _finite real-weighted WGraph, src be Vertex of G;
set DCS = DIJK:CompSeq(src), D0 = DCS.0;
defpred P[Nat] means (DCS.$1)`2 c= G.edgesBetween(dom ((DCS.$1)`1));
now
let n be Nat;
set Dn = DCS.n, Dn1 = DCS.(n+1);
set BE = DIJK:NextBestEdges(Dn), e = the Element of BE;
set target = (the_Target_of G).e;
set val= (Dn`1).((the_Source_of G).e)+(the_Weight_of G).e;
set DnE = Dn`2 \/ {e};
assume
A1: Dn`2 c= G.edgesBetween(dom Dn`1);
A2: Dn1 = DIJK:Step(Dn) by Def11;
now
let x be object;
n <= n+1 by NAT_1:12;
then
A3: dom Dn`1 c= dom Dn1`1 by Th18;
assume
A4: x in Dn1`2;
now
per cases;
suppose
BE = {};
then Dn1 = Dn by A2,Def8;
hence x in G.edgesBetween(dom Dn1`1) by A1,A4;
end;
suppose
A5: BE <> {};
then
A6: Dn1 = [Dn`1+*(target .--> val),DnE] by A2,Def8;
then
A7: Dn1`2 = DnE;
Dn1`1 = Dn`1+*(target .--> val) by A6;
then
A8: dom Dn1`1 = dom Dn`1 \/ {target} by Lm1;
A9: e in BE by A5;
now
per cases by A4,A7,XBOOLE_0:def 3;
suppose
A10: x in Dn`2;
(the_Source_of G).x in dom Dn`1 & (the_Target_of G).x in
dom Dn`1 by A1,A10,GLIB_000:31;
hence x in G.edgesBetween(dom Dn1`1) by A3,A10,GLIB_000:31;
end;
suppose
x in {e};
then
A11: x = e by TARSKI:def 1;
then (the_Target_of G).x in {target} by TARSKI:def 1;
then
A12: (the_Target_of G).x in dom Dn1`1 by A8,XBOOLE_0:def 3;
e DSJoins dom Dn`1,the_Vertices_of G \ dom Dn`1,G by A5,Def7;
then (the_Source_of G).x in dom Dn`1 by A11;
hence x in G.edgesBetween(dom Dn1`1) by A3,A9,A11,A12,GLIB_000:31
;
end;
end;
hence x in G.edgesBetween(dom Dn1`1);
end;
end;
hence x in G.edgesBetween(dom Dn1`1);
end;
hence Dn1`2 c= G.edgesBetween(dom Dn1`1);
end;
then
A13: for k being Nat st P[k] holds P[k+1];
D0=DIJK:Init(src) by Def11;
then for x being object st x in D0`2 holds x in G.edgesBetween(dom D0`1);
then
A14: P[ 0 ] by TARSKI:def 3;
for n being Nat holds P[n] from NAT_1:sch 2(A14,A13);
hence thesis;
end;
theorem Th23:
for G being _finite nonnegative-weighted WGraph, s being Vertex
of G, n being Nat, 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
let G be _finite nonnegative-weighted WGraph, src be Vertex of G;
set DCS = DIJK:CompSeq(src), D0 = DCS.0;
defpred P[Nat] means for G2 being inducedWSubgraph of G,dom (DCS.$1)`1,(DCS.
$1)`2 holds G2 is_mincost_DTree_rooted_at src & for v being Vertex of G st v in
dom (DCS.$1)`1 holds G.min_DPath_cost(src,v) = (DCS.$1)`1.v;
A1: D0 = DIJK:Init(src) by Def11;
then
A2: D0`1 = src .--> 0;
then
A3: dom D0`1 = {src};
now
let n be Nat;
set Dn = DCS.n, Dn1 = DCS.(n+1);
set BE = DIJK:NextBestEdges(Dn), e = the Element of BE;
set source = (the_Source_of G).e, target = (the_Target_of G).e;
set DnE = Dn`2 \/ {e};
set pc = Dn`1.source;
set ec = (the_Weight_of G).e;
set DnW = the inducedWSubgraph of G,dom Dn`1,Dn`2;
A4: Dn1 = DIJK:Step(Dn) by Def11;
assume
A5: P[n];
then
A6: DnW is_mincost_DTree_rooted_at src;
then
A7: DnW is Tree-like;
let Dn1W be inducedWSubgraph of G,dom Dn1`1, Dn1`2;
A8: src in dom D0`1 & dom D0`1 c= dom Dn`1 by A3,Th18,TARSKI:def 1;
A9: Dn`2 c= G.edgesBetween(dom Dn`1) by Th22;
then
A10: card Dn`2 = DnW.size() by A8,GLIB_000:def 37;
A11: Dn`2 c= G.edgesBetween(dom Dn`1) by Th22;
then
A12: the_Vertices_of DnW = dom Dn`1 by A8,GLIB_000:def 37;
A13: the_Edges_of DnW = Dn`2 by A8,A11,GLIB_000:def 37;
A14: card dom Dn`1 = DnW.order() by A8,A9,GLIB_000:def 37;
now
per cases;
suppose
BE = {};
then Dn1 = Dn by A4,Def8;
hence Dn1W is_mincost_DTree_rooted_at src & for v being Vertex of G st
v in dom Dn1`1 holds G.min_DPath_cost(src,v) = Dn1`1.v by A5;
end;
suppose
A15: BE <> {};
set mc = G.min_DPath_cost(src,target);
A16: the_Weight_of Dn1W = (the_Weight_of G)| the_Edges_of Dn1W by
GLIB_003:def 10;
A17: e DSJoins dom Dn`1, the_Vertices_of G \ dom Dn`1, G by A15,Def7;
then
A18: target in the_Vertices_of G\dom Dn`1;
then
A19: src <> target by A8,XBOOLE_0:def 5;
A20: not target in dom Dn`1 by A18,XBOOLE_0:def 5;
then
A21: card (dom Dn`1 \/ {target}) = card dom Dn`1 + 1 by CARD_2:41;
A22: source in dom Dn`1 by A17;
A23: Dn1 = [Dn`1+*(target .--> (pc+ec)), DnE] by A4,A15,Def8;
then Dn1`1 = Dn`1+*(target .--> (pc+ec));
then
A24: dom Dn1`1 = dom Dn`1 \/ {target} by Lm1;
A25: Dn1`2 c= G.edgesBetween(dom Dn1`1) by Th22;
then
A26: the_Vertices_of Dn1W = dom Dn`1 \/ {target} by A24,GLIB_000:def 37;
Dn1`2 = DnE by A23;
then
A27: the_Edges_of Dn1W =(Dn`2 \/ {e}) by A24,A25,GLIB_000:def 37;
A28: now
thus the_Vertices_of DnW c= the_Vertices_of Dn1W & the_Edges_of DnW
c= the_Edges_of Dn1W by A12,A13,A26,A27,XBOOLE_1:7;
let e be set;
assume
A29: e in the_Edges_of DnW;
then
A30: (the_Target_of DnW).e = (the_Target_of G).e by GLIB_000:def 32;
e in the_Edges_of Dn1W & (the_Source_of DnW).e = (the_Source_of
G).e by A13,A27,A29,GLIB_000:def 32,XBOOLE_0:def 3;
hence
(the_Source_of DnW).e = (the_Source_of Dn1W).e & (the_Target_of
DnW).e = (the_Target_of Dn1W).e by A30,GLIB_000:def 32;
end;
then reconsider DnW9 = DnW as [Weighted] Subgraph of Dn1W by
GLIB_000:def 32;
e in {e} by TARSKI:def 1;
then
A31: e in the_Edges_of Dn1W by A27,XBOOLE_0:def 3;
e in BE by A15;
then e DJoins source, target, G;
then
A32: e DJoins source, target, Dn1W by A31,GLIB_000:73;
then
A33: e Joins source, target, Dn1W;
A34: the_Weight_of DnW9 = (the_Weight_of G)| the_Edges_of DnW by
GLIB_003:def 10;
A35: now
let y be object;
assume y in dom the_Weight_of DnW9;
then
A36: y in the_Edges_of DnW;
hence (the_Weight_of DnW9).y = (the_Weight_of G).y by A34,FUNCT_1:49
.= (the_Weight_of Dn1W).y by A28,A16,A36,FUNCT_1:49;
end;
dom the_Weight_of Dn1W = the_Edges_of Dn1W by PARTFUN1:def 2;
then dom (the_Weight_of Dn1W)/\the_Edges_of DnW = the_Edges_of DnW by
A28,XBOOLE_1:28;
then dom the_Weight_of DnW9=dom (the_Weight_of Dn1W)/\ the_Edges_of
DnW by PARTFUN1:def 2;
then the_Weight_of DnW9 = (the_Weight_of Dn1W) | the_Edges_of DnW by
A35,FUNCT_1:46;
then
A37: DnW is WSubgraph of Dn1W by GLIB_003:def 10;
A38: DnW is Subgraph of Dn1W by A28,GLIB_000:def 32;
now
let u,v be Vertex of Dn1W;
A39: now
let u,v be set;
assume u in dom Dn`1 & v in dom Dn`1;
then reconsider u9=u, v9=v as Vertex of DnW by A11,GLIB_000:def 37;
consider W1 being Walk of DnW such that
A40: W1 is_Walk_from u9,v9 by A7,GLIB_002:def 1;
reconsider W2=W1 as Walk of Dn1W by A38,GLIB_001:167;
W2 is_Walk_from u,v by A40,GLIB_001:19;
hence ex W being Walk of Dn1W st W is_Walk_from u,v;
end;
now
per cases by A26,XBOOLE_0:def 3;
suppose
u in dom Dn`1 & v in dom Dn`1;
hence ex W being Walk of Dn1W st W is_Walk_from u,v by A39;
end;
suppose
A41: u in dom Dn`1 & v in {target};
then
A42: v = target by TARSKI:def 1;
consider W being Walk of Dn1W such that
A43: W is_Walk_from u,source by A22,A39,A41;
W.addEdge(e) is_Walk_from u,target by A33,A43,GLIB_001:66;
hence ex W being Walk of Dn1W st W is_Walk_from u,v by A42;
end;
suppose
A44: u in {target} & v in dom Dn`1;
then consider W being Walk of Dn1W such that
A45: W is_Walk_from v,source by A22,A39;
W.addEdge(e) is_Walk_from v,target by A33,A45,GLIB_001:66;
then W.addEdge(e) is_Walk_from v,u by A44,TARSKI:def 1;
then W.addEdge(e).reverse() is_Walk_from u,v by GLIB_001:23;
hence ex W being Walk of Dn1W st W is_Walk_from u,v;
end;
suppose
A46: u in {target} & v in {target};
take W = Dn1W.walkOf(u);
u = target & v = target by A46,TARSKI:def 1;
hence W is_Walk_from u,v by GLIB_001:13;
end;
end;
hence ex W being Walk of Dn1W st W is_Walk_from u,v;
end;
then
A47: Dn1W is connected by GLIB_002:def 1;
A48: not e in Dn`2 by A9,A20,GLIB_000:31;
then Dn1W.size() = DnW.size() + 1 by A10,A27,CARD_2:41;
then Dn1W.order() = Dn1W.size() + 1 by A14,A7,A26,A21,GLIB_002:47;
then
A49: Dn1W is Tree-like by A47,GLIB_002:47;
now
consider WT being DPath of DnW such that
A50: WT is_Walk_from src,source and
A51: for W1 being DPath of G st W1 is_Walk_from src,source
holds WT .cost() <= W1.cost() by A12,A6,A22;
reconsider WT9=WT as DPath of Dn1W by A38,GLIB_001:175;
set W2 = WT9.addEdge(e);
A52: WT9 is_Walk_from src,source by A50,GLIB_001:19;
then reconsider W2 as DWalk of Dn1W by A32,GLIB_001:123;
now
target in {target} by TARSKI:def 1;
hence target is Vertex of Dn1W by A26,XBOOLE_0:def 3;
thus e Joins WT9.last(),target,Dn1W by A33,A52,GLIB_001:def 23;
( not e in the_Edges_of DnW)& WT.edges() = WT9.edges() by A8,A9,A48
,GLIB_000:def 37,GLIB_001:110;
hence not e in WT9.edges();
thus WT9 is trivial or WT9 is open
by GLIB_001:def 31,A49,GLIB_002:def 2;
let n be odd Element of NAT;
assume that
1 < n and
A53: n <= len WT9;
WT9.vertices() = WT.vertices() by GLIB_001:98;
then not target in WT9.vertices() by A12,A18,XBOOLE_0:def 5;
hence WT9.n <> target by A53,GLIB_001:87;
end;
then reconsider W2 as DPath of Dn1W by GLIB_001:150;
take W2;
thus W2 is_Walk_from src,target by A33,A52,GLIB_001:66;
now
WT9.last() = source & (the_Source_of Dn1W).e = source by A32,A52,
GLIB_001:def 23;
hence e in WT9.last().edgesInOut() by A31,GLIB_000:61;
reconsider WTG = WT as DPath of G by GLIB_001:175;
A54: WTG is_Walk_from src,source by A50,GLIB_001:19;
(the_Weight_of Dn1W).e = ((the_Weight_of G) | the_Edges_of
Dn1W).e by GLIB_003:def 10;
hence ec = (the_Weight_of Dn1W).e by A31,FUNCT_1:49;
pc = G.min_DPath_cost(src,source) by A5,A22;
then consider WX being DPath of G such that
A55: WX is_mincost_DPath_from src,source and
A56: pc = WX.cost() by A54,Def3;
WX is_Walk_from src,source by A55;
then WT.cost() <= pc by A51,A56;
then
A57: WT9.cost() <= pc by A37,GLIB_003:27;
pc <= WTG.cost() by A54,A55,A56;
then pc <= WT9.cost() by GLIB_003:27;
hence WT9.cost() = pc by A57,XXREAL_0:1;
end;
hence W2.cost() = pc + ec by GLIB_003:25;
end;
then consider W2 being DPath of Dn1W such that
A58: W2 is_Walk_from src,target and
A59: W2.cost() = pc+ec;
reconsider W2G = W2 as DPath of G by GLIB_001:175;
A60: W2G is_Walk_from src, target by A58,GLIB_001:19;
A61: W2G.cost() = pc+ec by A59,GLIB_003:27;
now
consider WB being DPath of G such that
A62: WB is_mincost_DPath_from src,target and
A63: mc = WB.cost() by A60,Def3;
thus mc <= pc+ec by A60,A61,A62,A63;
A64: WB is_Walk_from src,target by A62;
then reconsider target9=target as Vertex of G by GLIB_001:18;
WB.first() = src & WB.last() = target by A64,GLIB_001:def 23;
then consider lenWB2h being odd Element of NAT such that
A65: lenWB2h = len WB - 2 and
A66: WB.cut(1,lenWB2h).addEdge(WB.(lenWB2h+1)) = WB by A19,GLIB_001:127
,133;
A67: lenWB2h < len WB - 0 by A65,XREAL_1:15;
set sa = WB.lenWB2h, ea = WB.(lenWB2h+1);
set WA = WB.cut(1,lenWB2h);
A68: 1 <= lenWB2h by ABIAN:12;
A69: WB.1 = WB.first() by GLIB_001:def 6
.= src by A64,GLIB_001:def 23;
then WA is_Walk_from src,sa by A68,A67,GLIB_001:37,JORDAN12:2;
then reconsider sa as Vertex of G by GLIB_001:18;
A70: ea DJoins sa, WB.(lenWB2h+2), G by A67,GLIB_001:122;
then
A71: ea DJoins sa, WB.last(), G by A65,GLIB_001:def 7;
then ea DJoins sa, target, G by A64,GLIB_001:def 23;
then ea Joins sa,target9,G;
then ea in sa.edgesInOut() by GLIB_000:62;
then
A72: ea in WA.last().edgesInOut() by A68,A67,GLIB_001:37,JORDAN12:2;
then
A73: mc = WA.cost() + (the_Weight_of G).ea by A63,A66,GLIB_003:25;
reconsider WA as DPath of G;
A74: WA.first() = src by A68,A67,A69,GLIB_001:37,JORDAN12:2;
A75: WA.last() = sa by A68,A67,GLIB_001:37,JORDAN12:2;
then
A76: WA is_mincost_DPath_from src,sa by A62,A74,Th12;
A77: ea DJoins sa, target, G by A64,A71,GLIB_001:def 23;
A78: WA.cost() = G.min_DPath_cost(src,sa) by A62,A74,A75,Th12,Th14;
now
defpred P[Nat] means $1 is odd & $1 <= len WA & not WA.$1 in dom
Dn`1;
A79: (the_Source_of G).ea = sa by A70;
assume
A80: mc < pc+ec;
A81: now
assume
A82: not sa in dom Dn`1;
sa = WA.last() by A68,A67,GLIB_001:37,JORDAN12:2
.= WA.(len WA) by GLIB_001:def 7;
then
A83: ex k being Nat st P[k] by A82;
consider k being Nat such that
A84: P[k] & for m being Nat st P[m] holds k <= m from NAT_1
:sch 5(A83);
reconsider k as odd Element of NAT by A84,ORDINAL1:def 12;
A85: 1 <= k by ABIAN:12;
WA.1 = WA.first() by GLIB_001:def 6
.= src by A68,A67,A69,GLIB_001:37,JORDAN12:2;
then k <> 1 by A8,A84;
then 1 < k by A85,XXREAL_0:1;
then 1+1 < k+1 by XREAL_1:8;
then 2 <= k by NAT_1:13;
then reconsider k2a = k-2*1 as odd Element of NAT by INT_1:5;
set sk = WA.k2a, ek = WA.(k2a+1), tk = WA.k;
A86: k2a < len WA - 0 by A84,XREAL_1:15;
set WKA = WA.cut(1,k), WKB = WA.cut(k,len WA);
set WK1 = WA.cut(1,k2a);
reconsider WK1, WKA, WKB as DPath of G;
A87: 1 <= k by ABIAN:12;
then
A88: WKA.append(WKB) = WA.cut(1,len WA) by A84,GLIB_001:38,JORDAN12:2
.= WA by GLIB_001:39;
A89: k2a < k - 0 by XREAL_1:15;
then
A90: sk in dom Dn`1 by A84,A86;
then reconsider sk as Vertex of G;
A91: 1 <= k2a by ABIAN:12;
then
A92: WK1.last() = sk by A86,GLIB_001:37,JORDAN12:2;
WK1.first() = WA.1 by A91,A86,GLIB_001:37,JORDAN12:2;
then WK1 is_mincost_DPath_from WA.1, sk by A76,A92,Th12;
then WK1 is_mincost_DPath_from WA.first(),sk by GLIB_001:def 6;
then G.min_DPath_cost(src,sk) = WK1.cost() by A74,Th14;
then
A93: Dn`1.sk = WK1.cost() by A5,A84,A86,A89;
reconsider tk as Vertex of G by A84,GLIB_001:7;
A94: tk in the_Vertices_of G \ dom Dn`1 by A84,XBOOLE_0:def 5;
tk = WA.(k2a+2);
then
A95: ek DJoins sk,tk,G by A86,GLIB_001:122;
then
A96: (the_Source_of G).ek = sk;
WKB.first() = WA.k by A84,GLIB_001:37
.= WKA.last() by A84,A87,GLIB_001:37,JORDAN12:2;
then
A97: WA.cost() = WKA.cost() + WKB.cost() by A88,GLIB_003:24;
0 <= WKB.cost() by GLIB_003:29;
then
A98: 0 qua Nat + WKA.cost() <= WA.cost() by A97,XREAL_1:7;
ea in the_Edges_of G by A70;
then
A99: 0 <= (the_Weight_of G).ea by GLIB_003:31;
ek in the_Edges_of G & (the_Target_of G).ek = tk by A95;
then ek DSJoins dom Dn`1,the_Vertices_of G \ dom Dn`1,G by A90
,A96,A94;
then
A100: pc+ec <= WK1.cost() + (the_Weight_of G).ek by A15,A96,A93,Def7;
ek in the_Edges_of G & (the_Source_of G).ek = sk by A95;
then
A101: ek in sk.edgesInOut() by GLIB_000:61;
k2a + 2 = k;
then WK1.addEdge(ek) = WKA by A86,ABIAN:12,GLIB_001:41,JORDAN12:2
;
then pc+ec <= WKA.cost() by A92,A100,A101,GLIB_003:25;
then pc+ec <= WA.cost() by A98,XXREAL_0:2;
then pc+ec+(0 qua Nat) <= WA.cost()+(the_Weight_of G).ea by A99,
XREAL_1:7;
hence contradiction by A63,A66,A72,A80,GLIB_003:25;
end;
then
A102: WA.cost() = Dn`1.sa by A5,A78;
ea in the_Edges_of G & (the_Target_of G).ea=target by A77;
then ea DSJoins dom Dn`1, the_Vertices_of G \ dom Dn`1,G by A18,A81
,A79;
hence contradiction by A15,A73,A80,A102,A79,Def7;
end;
hence mc >= pc+ec;
end;
then
A103: G.min_DPath_cost(src,target) = pc+ec by XXREAL_0:1;
now
let x be Vertex of Dn1W;
now
per cases by A26,XBOOLE_0:def 3;
suppose
x in dom Dn`1;
then reconsider x9=x as Vertex of DnW by A11,GLIB_000:def 37;
DnW is_mincost_DTree_rooted_at src by A5;
then consider W2 being DPath of DnW such that
A104: W2 is_Walk_from src,x9 and
A105: for W1 being DPath of G st W1 is_Walk_from src,x9
holds W2.cost() <= W1.cost();
reconsider W29=W2 as DPath of Dn1W by A38,GLIB_001:175;
take W29;
thus W29 is_Walk_from src,x by A104,GLIB_001:19;
let W1 be DPath of G;
assume W1 is_Walk_from src,x;
then W2.cost() <= W1.cost() by A105;
hence W29.cost() <= W1.cost() by A37,GLIB_003:27;
end;
suppose
A106: x in {target};
take W2;
thus W2 is_Walk_from src,x by A58,A106,TARSKI:def 1;
let W1 be DPath of G;
assume
A107: W1 is_Walk_from src,x;
A108: x = target by A106,TARSKI:def 1;
ex WX being DPath of G st WX is_mincost_DPath_from src,
target & WX.cost()=W2 .cost() by A59,A60,A103,Def3;
hence W2.cost() <= W1.cost() by A108,A107;
end;
end;
hence ex W2 being DPath of Dn1W st W2 is_Walk_from src,x & for W1
being DPath of G st W1 is_Walk_from src,x holds W2.cost() <= W1.cost();
end;
hence Dn1W is_mincost_DTree_rooted_at src by A49;
let v be Vertex of G;
assume
A109: v in dom Dn1`1;
now
per cases by A24,A109,XBOOLE_0:def 3;
suppose
A110: v in dom Dn`1;
then
A111: G.min_DPath_cost(src,v) = Dn`1.v by A5;
A112: Dn1`1 = Dn`1+*(target .-->(pc+ec)) by A23;
not v in dom (target .-->(pc+ec)) by A20,A110,TARSKI:def 1;
hence
G.min_DPath_cost(src,v)=(Dn1`1).v by A24,A109,A111,A112,
FUNCT_4:def 1;
end;
suppose
A114: v in {target};
Dn1`1 = Dn`1+*(target .-->(pc+ec)) & dom (target .--> (pc+ec
)) = {target} by A23;
then
A115: (Dn1`1).v = (target .--> (pc+ec)).v by A114,FUNCT_4:13;
v = target by A114,TARSKI:def 1;
hence G.min_DPath_cost(src,v) = (Dn1`1).v by A103,A115,FUNCOP_1:72;
end;
end;
hence G.min_DPath_cost(src,v) = (Dn1`1).v;
end;
end;
hence
Dn1W is_mincost_DTree_rooted_at src & for v being Vertex of G st v in
dom Dn1`1 holds G.min_DPath_cost(src,v) = (Dn1`1).v;
end;
then
A116: for k being Nat st P[k] holds P[k+1];
A117: D0`2 = {} by A1;
now
let D0W be inducedWSubgraph of G,dom D0`1,D0`2;
A118: {} c= G.edgesBetween(dom D0`1);
then
A119: the_Vertices_of D0W = {src} by A3,A117,GLIB_000:def 37;
then card (the_Vertices_of D0W) = 1 by CARD_1:30;
then
A120: D0W is _trivial;
A121: now
let x be Vertex of D0W;
set W2 = D0W.walkOf(x);
take W2;
x = src by A119,TARSKI:def 1;
hence W2 is_Walk_from src,x by GLIB_001:13;
let W1 be DPath of G;
assume W1 is_Walk_from src,x;
0 <= W1.cost() by GLIB_003:29;
hence W2.cost() <= W1.cost() by GLIB_003:21;
end;
the_Edges_of D0W = {} by A2,A117,A118,GLIB_000:def 37;
then D0W.order() = D0W.size() + 1 by A119,CARD_1:30;
then D0W is Tree-like by A120,GLIB_002:47;
hence D0W is_mincost_DTree_rooted_at src by A121;
let v be Vertex of G;
assume
A122: v in dom D0`1;
then
A123: v = src by A3,TARSKI:def 1;
A124: now
set W1 = G.walkOf(v);
A125: W1 is_Walk_from src,v by A123,GLIB_001:13;
then consider W being DPath of G such that
A126: W is_mincost_DPath_from src,v and
A127: G.min_DPath_cost(src,v) = W.cost() by Def3;
W1.cost() = 0 by GLIB_003:21;
then W.cost() <= 0 by A125,A126;
hence G.min_DPath_cost(src,v) = 0 by A127,GLIB_003:29;
end;
D0`1.src = 0 by A2;
hence G.min_DPath_cost(src,v) = D0`1.v by A3,A122,A124,TARSKI:def 1;
end;
then
A128: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A128,A116);
hence thesis;
end;
theorem Th24:
for G being _finite real-weighted WGraph, s being Vertex of G
holds DIJK:CompSeq(s) is halting
proof
let G be _finite real-weighted WGraph, src be Vertex of G;
set DCS = DIJK:CompSeq( src);
now
set RSize = card G.reachableDFrom(src);
take n = card G.reachableDFrom(src);
set Gn = DCS.n, Gn1a = DCS.(n+1);
set BestEdges = DIJK:NextBestEdges(Gn);
A1: Gn1a = DIJK:Step(Gn) by Def11;
now
per cases;
suppose
BestEdges = {};
hence DCS.n = DCS.(n+1) by A1,Def8;
end;
suppose
A2: BestEdges <> {};
card dom (DCS.n)`1 = min(n+1, RSize) & RSize <= RSize + 1 by Th21,
NAT_1:11;
then
A3: card dom Gn`1 = RSize by XXREAL_0:def 9;
RSize + 1 <= RSize + 1 + 1 & RSize <= (RSize+1) by NAT_1:11;
then
A4: RSize <= (n + 1) + 1 by XXREAL_0:2;
A5: card dom Gn1a`1 = min((n+1)+1, RSize) by Th21
.= RSize by A4,XXREAL_0:def 9;
card dom (DIJK:Step(Gn))`1 = card dom Gn`1 + 1 by A2,Th15;
hence DCS.n = DCS.(n+1) by A3,A5,Def11;
end;
end;
hence DCS.n = DCS.(n+1);
end;
hence thesis;
end;
registration
let G be _finite real-weighted WGraph, src be Vertex of G;
cluster DIJK:CompSeq(src) -> halting;
coherence by Th24;
end;
theorem Th25:
for G being _finite real-weighted WGraph, s being Vertex of G
holds DIJK:CompSeq(s).Lifespan() + 1 = card G.reachableDFrom(s)
proof
let G be _finite real-weighted WGraph, src be Vertex of G;
set DCS = DIJK:CompSeq(src), RFS = G.reachableDFrom(src);
consider k being Nat such that
A1: card RFS = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A2: now
let n be Nat;
set Gn = DCS.n, Gn1 = DCS.(n+1);
assume
A3: DCS.n = DCS.(n+1);
now
assume n < k;
then
A4: n + 1 < card RFS by A1,XREAL_1:8;
then
A5: n + 1 + 1 <= card RFS by NAT_1:13;
card dom Gn`1 = min(n+1, card RFS) by Th21;
then
A6: card dom Gn`1 = n+1 by A4,XXREAL_0:def 9;
card dom Gn1`1 = min(n+1+1, card RFS) by Th21;
then 0+(n+1) = 1+(n+1) by A3,A6,A5,XXREAL_0:def 9;
hence contradiction;
end;
hence k <= n;
end;
set Gk = DCS.k, Gk1 = DCS.(k+1);
A7: card RFS <= card RFS + 1 by NAT_1:11;
A8: Gk1 = DIJK:Step(Gk) by Def11;
card dom Gk1`1 = min(card RFS+1, card RFS) & card dom Gk`1 = min(card
RFS, card RFS) by A1,Th21;
then card dom Gk1`1 = card dom Gk`1 by A7,XXREAL_0:def 9;
then DIJK:NextBestEdges(Gk) = {} by A8,Th15;
then DCS.k = DCS.(k+1) by A8,Def8;
hence thesis by A1,A2,GLIB_000:def 56;
end;
theorem Th26:
for G being _finite real-weighted WGraph, s being Vertex of G
holds dom (DIJK:SSSP(G,s))`1 = G.reachableDFrom(s)
proof
let G be _finite real-weighted WGraph, src be Vertex of G;
set Gn = DIJK:SSSP(G, src), RFS = G.reachableDFrom(src);
set DCS = DIJK:CompSeq(src), n = DCS.Lifespan();
A1: card (dom Gn`1) = min(n+1, card RFS) by Th21
.= min(card RFS, card RFS) by Th25
.= card RFS;
now
assume
A2: dom Gn`1 <> RFS;
dom Gn`1 c= RFS by Th19;
then dom Gn`1 c< RFS by A2,XBOOLE_0:def 8;
hence contradiction by A1,TREES_1:6;
end;
hence thesis;
end;
::$N Dijkstra's shortest path algorithm
theorem
for G being _finite nonnegative-weighted WGraph, s being Vertex of G,
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
let G be _finite nonnegative-weighted WGraph, src be Vertex of G, G2 be
inducedWSubgraph of G, dom (DIJK:SSSP(G,src))`1, DIJK:SSSP(G,src)`2;
set Res = DIJK:SSSP(G,src);
set dR = dom Res`1;
thus G2 is_mincost_DTree_rooted_at src by Th23;
let v being Vertex of G;
assume v in G.reachableDFrom(src);
then
A1: v in dR by Th26;
Res`2 c= G.edgesBetween(dR) by Th22;
hence v in the_Vertices_of G2 by A1,GLIB_000:def 37;
thus thesis by A1,Th23;
end;
begin :: Prim's Algorithm definitions
definition
let G be _Graph;
mode PRIM:Labeling of G is Element of [: bool the_Vertices_of G, bool
the_Edges_of G :];
end;
registration
let G be _finite _Graph, L be PRIM:Labeling of G;
cluster L`1 -> finite for set;
coherence;
cluster L`2 -> finite for set;
coherence;
end;
definition
let G be real-weighted WGraph, L being PRIM:Labeling of G;
func PRIM:NextBestEdges(L) -> Subset of the_Edges_of G means
:Def13:
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
proof
defpred P[set] means $1 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).
$1 <= (the_Weight_of G).e2;
consider IT being Subset of the_Edges_of G such that
A1: for e1 being set holds e1 in IT iff e1 in the_Edges_of G & P[e1]
from SUBSET_1:sch 1;
take IT;
let e1 be set;
thus e1 in IT implies P[e1] by A1;
assume
A2: P[e1];
then e1 in the_Edges_of G by GLIB_000:def 15;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred P[set] means $1 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).
$1 <= (the_Weight_of G).e2;
let IT1, IT2 be Subset of the_Edges_of G such that
A3: for e1 being set holds e1 in IT1 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 and
A4: for e1 being set holds e1 in IT2 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;
now
let e1 be object;
reconsider ee=e1 as set by TARSKI:1;
hereby
assume e1 in IT1;
then P[ee] by A3;
hence e1 in IT2 by A4;
end;
assume e1 in IT2;
then P[ee] by A4;
hence e1 in IT1 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let G be real-weighted WGraph;
func PRIM:Init(G) -> PRIM:Labeling of G equals
[ {the Element of the_Vertices_of G}, {} ];
coherence
proof
{} c= the_Edges_of G;
hence thesis by ZFMISC_1:def 2;
end;
end;
definition
let G be real-weighted WGraph, L being PRIM:Labeling of G;
func PRIM:Step(L) -> PRIM:Labeling of G equals
:Def15:
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
proof
set V = the_Vertices_of G, E = the_Edges_of G;
set BE = PRIM:NextBestEdges(L), e = the Element of BE;
set s = (the_Source_of G).e, t = (the_Target_of G).e;
A1: now
assume that
A2: BE <> {} and
not (the_Source_of G).e in L`1;
e in BE by A2;
then reconsider s9 = s as Element of V by FUNCT_2:5;
A3: L`1 \/ {s9} c= V;
A4: {e} c= E
proof
let x be object;
assume x in {e};
then x = e by TARSKI:def 1;
then x in BE by A2;
hence thesis;
end;
L`2 \/ {e} c= E by A4,XBOOLE_1:8;
hence [L`1 \/ {s}, L`2 \/ {e}] is PRIM:Labeling of G by A3,ZFMISC_1:def 2
;
end;
now
assume that
A5: BE <> {} and
(the_Source_of G).e in L`1;
e in BE by A5;
then reconsider t9 = t as Element of V by FUNCT_2:5;
A6: L`1 \/ {t9} c= V;
A7: {e} c= E
proof
let x be object;
assume x in {e};
then x = e by TARSKI:def 1;
then x in BE by A5;
hence thesis;
end;
L`2 \/ {e} c= E by A7,XBOOLE_1:8;
hence [L`1 \/ {t}, L`2 \/ {e}] is PRIM:Labeling of G by A6,ZFMISC_1:def 2
;
end;
hence thesis by A1;
end;
consistency;
end;
definition
let G be real-weighted WGraph;
mode PRIM:LabelingSeq of G -> ManySortedSet of NAT means
:Def16:
for n being Nat holds it.n is PRIM:Labeling of G;
existence
proof
defpred P[object,object] means $2 is PRIM:Labeling of G;
:: !!! funkcja stala
A1: now
let i be object;
assume i in NAT;
reconsider r = [{},{}] as object;
take r;
{} c= the_Vertices_of G & {} c= the_Edges_of G;
hence P[i,r] by ZFMISC_1:def 2;
end;
consider s being ManySortedSet of NAT such that
A2: for i being object st i in NAT holds P[i,s.i] from PBOOLE:sch 3(A1);
take s;
let i be Nat;
i in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
end;
definition
let G be real-weighted WGraph, S be PRIM:LabelingSeq of G, n be Nat;
redefine func S.n -> PRIM:Labeling of G; :: redefines . (FUNCT_1, definition)
coherence by Def16;
end;
definition
let G be real-weighted WGraph;
func PRIM:CompSeq(G) -> PRIM:LabelingSeq of G means
:Def17:
it.0 = PRIM:Init (G) & for n being Nat holds it.(n+1) = PRIM:Step(it.n);
existence
proof
defpred P[set,set,set] means ($2 is PRIM:Labeling of G & ex Gn,Gn1 being
PRIM:Labeling of G st $2 = Gn & $3 = Gn1 & Gn1 = PRIM:Step(Gn)) or (not $2 is
PRIM:Labeling of G & $2 = $3);
now
let n be Nat, x be set;
per cases;
suppose
x is PRIM:Labeling of G;
then reconsider Gn = x as PRIM:Labeling of G;
P[n,x,PRIM:Step(Gn)];
hence ex y being set st P[n,x,y];
end;
suppose
not x is PRIM:Labeling of G;
hence ex y being set st P[n,x,y];
end;
end;
then
A1: for n being Nat for x being set ex y being set st P[n,x,y];
consider IT being Function such that
A2: dom IT = NAT & IT.0 = PRIM:Init(G) & for n being Nat
holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
reconsider IT as ManySortedSet of NAT by A2,PARTFUN1:def 2,RELAT_1:def 18;
defpred P2[Nat] means IT.$1 is PRIM:Labeling of G;
A3: now
let n be Nat;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume P2[n];
then
ex Gn,Gn1 being PRIM:Labeling of G st IT.n9 = Gn & IT.(n +1) = Gn1 &
Gn1 = PRIM:Step(Gn) by A2;
hence P2[n+1];
end;
A4: P2[ 0 ] by A2;
for n being Nat holds P2[n] from NAT_1:sch 2(A4,A3);
then reconsider IT as PRIM:LabelingSeq of G by Def16;
take IT;
thus IT.0 = PRIM:Init(G) by A2;
let n be Nat;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
ex Gn,Gn1 being PRIM:Labeling of G st IT.n9 = Gn & IT.(n +1) = Gn1 &
Gn1 = PRIM:Step(Gn) by A2;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be PRIM:LabelingSeq of G such that
A5: IT1.0 = PRIM:Init(G) and
A6: for n being Nat holds IT1.(n+1) = PRIM:Step(IT1.n) and
A7: IT2.0 = PRIM:Init(G) and
A8: for n being Nat holds IT2.(n+1) = PRIM:Step(IT2.n);
defpred P[Nat] means IT1.$1 = IT2.$1;
now
let n be Nat;
assume P[n];
then IT1.(n+1) = PRIM:Step(IT2.n) by A6
.= IT2.(n+1) by A8;
hence P[n+1];
end;
then
A9: for n being Nat st P[n] holds P[n+1];
A10: P[ 0 ] by A5,A7;
for n being Nat holds P[n] from NAT_1:sch 2(A10,A9);
then for n being object st n in NAT holds IT1.n = IT2.n;
hence IT1 = IT2 by PBOOLE:3;
end;
end;
definition
let G be real-weighted WGraph;
func PRIM:MST(G) -> PRIM:Labeling of G equals
PRIM:CompSeq(G).Result();
coherence
proof
set PCS = PRIM:CompSeq(G);
PCS.Result() = PCS.(PCS.Lifespan());
hence thesis;
end;
end;
theorem Th28:
for G being real-weighted WGraph, L be 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
let G be real-weighted WGraph, L be PRIM:Labeling of G;
set G2 = PRIM:Step(L);
set e = the Element of PRIM:NextBestEdges(L);
set src = (the_Source_of G).e, tar = (the_Target_of G).e;
assume
A1: PRIM:NextBestEdges(L) <> {};
then e in PRIM:NextBestEdges(L);
then reconsider src,tar as Vertex of G by FUNCT_2:5;
A2: e SJoins L`1, the_Vertices_of G \ L`1, G by A1,Def13;
now
per cases;
suppose
A3: src in L`1;
take tar;
not src in the_Vertices_of G \ L`1 by A3,XBOOLE_0:def 5;
then tar in the_Vertices_of G \ L`1 by A2;
hence not tar in L`1 by XBOOLE_0:def 5;
thus G2 = [L`1 \/ {tar}, L`2 \/ {e}] by A1,A3,Def15;
end;
suppose
A4: not src in L`1;
take src;
thus not src in L`1 by A4;
thus G2 = [L`1 \/ {src}, L`2 \/ {e}] by A1,A4,Def15;
end;
end;
hence thesis;
end;
theorem Th29:
for G being real-weighted WGraph, L be PRIM:Labeling of G holds
L`1 c= (PRIM:Step(L))`1 & L`2 c= (PRIM:Step(L))`2
proof
let G be real-weighted WGraph, L be PRIM:Labeling of G;
set G2 = PRIM:Step(L);
set Next = PRIM:NextBestEdges(L), e = the Element of Next;
now
per cases;
suppose
Next = {};
hence thesis by Def15;
end;
suppose
Next <> {};
then consider v being Vertex of G such that
not v in L`1 and
A1: G2 = [L`1 \/ {v}, L`2 \/ {e}] by Th28;
G2`1 = L`1 \/ {v} by A1;
hence L`1 c= G2`1 by XBOOLE_1:7;
G2`2 = L`2 \/ {e} by A1;
hence L`2 c= G2`2 by XBOOLE_1:7;
end;
end;
hence thesis;
end;
theorem Th30:
for G being _finite real-weighted WGraph, 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
let G be _finite real-weighted WGraph;
set PCS = PRIM:CompSeq(G);
defpred P[Nat] means (PCS.$1)`1 is non empty Subset of the_Vertices_of G & (
PCS.$1)`2 c= G.edgesBetween((PCS.$1)`1);
A1: (PCS.0)`2 = (PRIM:Init(G))`2 by Def17
.= {};
now
let n be Nat;
assume
A2: P[n];
set Gn = PCS.n, Gn1 = PCS.(n+1);
set Next = PRIM:NextBestEdges(Gn), e = the Element of Next;
A3: Gn1 = PRIM:Step(Gn) by Def17;
now
per cases;
suppose
Next = {};
then Gn1 = Gn by A3,Def15;
hence P[n+1] by A2;
end;
suppose
A4: Next <> {};
set src = (the_Source_of G).e, tar = (the_Target_of G).e;
A5: e in Next by A4;
A6: e SJoins Gn`1, the_Vertices_of G \ Gn`1, G by A4,Def13;
now
per cases;
suppose
A7: (the_Source_of G).e in Gn`1;
then
A8: Gn1 = [Gn`1 \/ {tar}, Gn`2 \/ {e}] by A3,A4,Def15;
then
A9: Gn1`1 = Gn`1 \/ {tar};
then
A10: G.edgesBetween(Gn`1) c= G.edgesBetween(Gn1`1) by GLIB_000:36
,XBOOLE_1:7;
thus Gn1`1 is non empty Subset of the_Vertices_of G by A8
;
A11: Gn1`2 = Gn`2 \/ {e} by A8;
A12: Gn`1 c= Gn1`1 by A9,XBOOLE_1:7;
now
let x be object;
assume
A13: x in Gn1`2;
now
per cases by A11,A13,XBOOLE_0:def 3;
suppose
x in Gn`2;
then x in G.edgesBetween(Gn`1) by A2;
hence x in G.edgesBetween(Gn1`1) by A10;
end;
suppose
x in {e};
then
A14: x = e by TARSKI:def 1;
then (the_Target_of G).x in {tar} by TARSKI:def 1;
then (the_Target_of G).x in Gn1`1 by A9,XBOOLE_0:def 3;
hence x in G.edgesBetween(Gn1`1) by A5,A7,A12,A14,GLIB_000:31
;
end;
end;
hence x in G.edgesBetween(Gn1`1);
end;
hence Gn1`2 c= G.edgesBetween(Gn1`1);
end;
suppose
A15: not (the_Source_of G).e in Gn`1;
then
A16: tar in Gn`1 by A6;
A17: Gn1 = [Gn`1 \/ {(the_Source_of G).e}, Gn`2 \/ {e}] by A3,A4,A15
,Def15;
then
A18: Gn1`1 = Gn`1 \/ {src};
then
A19: G.edgesBetween(Gn`1) c= G.edgesBetween(Gn1`1) by GLIB_000:36
,XBOOLE_1:7;
thus Gn1`1 is non empty Subset of the_Vertices_of G by A17;
A20: Gn1`2 = Gn`2 \/ {e} by A17;
A21: Gn`1 c= Gn1`1 by A18,XBOOLE_1:7;
now
let x be object;
assume
A22: x in Gn1`2;
now
per cases by A20,A22,XBOOLE_0:def 3;
suppose
x in Gn`2;
then x in G.edgesBetween(Gn`1) by A2;
hence x in G.edgesBetween(Gn1`1) by A19;
end;
suppose
x in {e};
then
A23: x = e by TARSKI:def 1;
then (the_Source_of G).x in {src} by TARSKI:def 1;
then (the_Source_of G).x in Gn1`1 by A18,XBOOLE_0:def 3;
hence x in G.edgesBetween(Gn1`1) by A5,A21,A16,A23,
GLIB_000:31;
end;
end;
hence x in G.edgesBetween(Gn1`1);
end;
hence Gn1`2 c= G.edgesBetween(Gn1`1);
end;
end;
hence P[n+1];
end;
end;
hence P[n+1];
end;
then
A24: for n being Nat st P[n] holds P[n+1];
(PCS.0)`1 = (PRIM:Init(G))`1 by Def17
.= {the Element of the_Vertices_of G};
then
A25: P[ 0 ] by A1,XBOOLE_1:2;
for n being Nat holds P[n] from NAT_1:sch 2(A25,A24);
hence thesis;
end;
theorem Th31:
for G1 being _finite real-weighted WGraph, n being Nat, G2 being
inducedSubgraph of G1,(PRIM:CompSeq(G1).n)`1, (PRIM:CompSeq(G1).n)`2 holds G2
is connected
proof
let G1 be _finite real-weighted WGraph;
defpred P[Nat] means for G2 being inducedSubgraph of G1, (PRIM:CompSeq(G1).
$1)`1, (PRIM:CompSeq(G1).$1)`2 holds G2 is connected;
set G0 = PRIM:CompSeq(G1).0, v = the Element of the_Vertices_of G1;
now
let n be Nat;
assume
A1: P[n];
set Gn = PRIM:CompSeq(G1).n, Gn1 = PRIM:CompSeq(G1).(n+1);
set e = the Element of PRIM:NextBestEdges(Gn);
set v1 = (the_Target_of G1).e, v2 = (the_Source_of G1).e;
A2: Gn1 = PRIM:Step(Gn) by Def17;
now
let Gn1s be inducedSubgraph of G1, Gn1`1, Gn1`2;
A3: Gn1`1 is non empty Subset of the_Vertices_of G1 & Gn1`2c=G1
.edgesBetween(Gn1 `1) by Th30;
then
A4: the_Vertices_of Gn1s = Gn1`1 by GLIB_000:def 37;
A5: the_Edges_of Gn1s = Gn1`2 by A3,GLIB_000:def 37;
now
per cases;
suppose
PRIM:NextBestEdges(Gn) = {};
then Gn1 = Gn by A2,Def15;
hence Gn1s is connected by A1;
end;
suppose
A6: PRIM:NextBestEdges(Gn) <> {} & v2 in Gn`1;
then
A7: Gn1 = [Gn`1 \/ {v1}, Gn`2 \/ {e} ] by A2,Def15;
then
A8: Gn1`2 = Gn`2 \/ {e};
A9: e in PRIM:NextBestEdges(Gn) by A6;
then reconsider v1 as Vertex of G1 by FUNCT_2:5;
A10: e Joins v2,v1,G1 by A9;
set Gns = the inducedSubgraph of G1,Gn`1,Gn`2;
A11: Gns is connected by A1;
A12: Gn`1 is non empty Subset of the_Vertices_of G1 & Gn`2 c= G1
.edgesBetween(Gn `1) by Th30;
then
A13: the_Vertices_of Gns = Gn`1 by GLIB_000:def 37;
A14: Gn1`1 = Gn`1 \/ {v1} by A7;
then
A15: the_Vertices_of Gns c= the_Vertices_of Gn1s by A4,A13,XBOOLE_1:7;
the_Edges_of Gns = Gn`2 by A12,GLIB_000:def 37;
then reconsider Gns as Subgraph of Gn1s by A5,A8,A15,GLIB_000:44
,XBOOLE_1:7;
set src = the Vertex of Gns;
reconsider src9 = src as Vertex of Gn1s by GLIB_000:42;
e in {e} by TARSKI:def 1;
then e in the_Edges_of Gn1s by A5,A8,XBOOLE_0:def 3;
then
A16: e Joins v2,v1,Gn1s by A10,GLIB_000:73;
now
let x be Vertex of Gn1s;
now
per cases;
suppose
A17: x = v1;
reconsider v29=v2 as Vertex of Gns by A6,A12,GLIB_000:def 37;
consider W being Walk of Gns such that
A18: W is_Walk_from src,v29 by A11,GLIB_002:def 1;
reconsider W as Walk of Gn1s by GLIB_001:167;
W is_Walk_from src9,v2 by A18,GLIB_001:19;
then W.addEdge(e) is_Walk_from src9,x by A16,A17,GLIB_001:66;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x;
end;
suppose
x <> v1;
then not x in {v1} by TARSKI:def 1;
then reconsider x9=x as Vertex of Gns by A4,A14,A13,
XBOOLE_0:def 3;
consider W being Walk of Gns such that
A19: W is_Walk_from src,x9 by A11,GLIB_002:def 1;
reconsider W9=W as Walk of Gn1s by GLIB_001:167;
W9 is_Walk_from src9,x by A19,GLIB_001:19;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x;
end;
end;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x;
end;
hence Gn1s is connected by GLIB_002:6;
end;
suppose
A20: PRIM:NextBestEdges(Gn) <> {} & not v2 in Gn`1;
then
A21: Gn1 = [Gn`1 \/ {v2}, Gn`2 \/ {e}] by A2,Def15;
then
A22: Gn1`2 = Gn`2 \/ {e};
A23: e SJoins Gn`1,the_Vertices_of G1\Gn`1,G1 by A20,Def13;
then
A24: e in the_Edges_of G1;
then reconsider v2 as Vertex of G1 by FUNCT_2:5;
A25: e Joins v1,v2,G1 by A24;
e in {e} by TARSKI:def 1;
then e in the_Edges_of Gn1s by A5,A22,XBOOLE_0:def 3;
then
A26: e Joins v1,v2,Gn1s by A25,GLIB_000:73;
set Gns = the inducedSubgraph of G1,Gn`1,Gn`2;
A27: Gns is connected by A1;
A28: Gn`1 is non empty Subset of the_Vertices_of G1 & Gn`2c= G1
.edgesBetween(Gn`1 ) by Th30;
then
A29: the_Vertices_of Gns = Gn`1 by GLIB_000:def 37;
A30: Gn1`1 = Gn`1 \/ {v2} by A21;
then
A31: the_Vertices_of Gns c= the_Vertices_of Gn1s by A4,A29,XBOOLE_1:7;
the_Edges_of Gns = Gn`2 by A28,GLIB_000:def 37;
then reconsider Gns as Subgraph of Gn1s by A5,A22,A31,GLIB_000:44
,XBOOLE_1:7;
set src = the Vertex of Gns;
reconsider src9 = src as Vertex of Gn1s by GLIB_000:42;
A32: v1 in Gn`1 by A20,A23;
now
let x be Vertex of Gn1s;
now
per cases;
suppose
A33: x = v2;
reconsider v19=v1 as Vertex of Gns by A32,A28,GLIB_000:def 37;
consider W being Walk of Gns such that
A34: W is_Walk_from src,v19 by A27,GLIB_002:def 1;
reconsider W as Walk of Gn1s by GLIB_001:167;
W is_Walk_from src9,v1 by A34,GLIB_001:19;
then W.addEdge(e) is_Walk_from src9,x by A26,A33,GLIB_001:66;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x;
end;
suppose
x <> v2;
then not x in {v2} by TARSKI:def 1;
then reconsider x9=x as Vertex of Gns by A4,A30,A29,
XBOOLE_0:def 3;
consider W being Walk of Gns such that
A35: W is_Walk_from src,x9 by A27,GLIB_002:def 1;
reconsider W9=W as Walk of Gn1s by GLIB_001:167;
W9 is_Walk_from src9,x by A35,GLIB_001:19;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x;
end;
end;
hence ex W being Walk of Gn1s st W is_Walk_from src9,x;
end;
hence Gn1s is connected by GLIB_002:6;
end;
end;
hence Gn1s is connected;
end;
hence P[n+1];
end;
then
A36: for n being Nat st P[n] holds P[n+1];
now
let G be inducedSubgraph of G1, G0`1, G0`2;
G0 = PRIM:Init(G1) by Def17;
then reconsider G9 = G as inducedSubgraph of G1,{v},{};
G9 is connected;
hence G is connected;
end;
then
A38: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A38,A36);
hence thesis;
end;
theorem Th32:
for G1 being _finite real-weighted WGraph, n being Nat, G2 being
inducedSubgraph of G1, (PRIM:CompSeq(G1).n)`1 holds G2 is connected
proof
let G1 be _finite real-weighted WGraph, n be Nat;
set V = (PRIM:CompSeq(G1).n)`1;
let G2 be inducedSubgraph of G1, V;
reconsider V as non empty Subset of the_Vertices_of G1 by Th30;
set E = (PRIM:CompSeq(G1).n)`2;
reconsider E as Subset of G1.edgesBetween(V) by Th30;
set G3 = the inducedSubgraph of G1,V,E;
A1: the_Vertices_of G3 = V & the_Vertices_of G2 = V by GLIB_000:def 37;
the_Edges_of G3 = E & the_Edges_of G2 = G1.edgesBetween(V) by GLIB_000:def 37
;
then reconsider G3 as Subgraph of G2 by A1,GLIB_000:44;
A2: G3 is spanning by A1;
G3 is connected by Th31;
hence thesis by A2,GLIB_002:23;
end;
registration
let G1 be _finite real-weighted WGraph, n be Nat;
cluster -> connected for inducedSubgraph of G1,(PRIM:CompSeq(G1).n)`1;
coherence by Th32;
end;
registration
let G1 be _finite real-weighted WGraph, n be Nat;
cluster -> connected for inducedSubgraph of G1, (PRIM:CompSeq(G1).n)`1, (
PRIM:CompSeq(G1).n)`2;
coherence by Th31;
end;
theorem Th33:
for G being _finite real-weighted WGraph, n being Nat holds (
PRIM:CompSeq(G).n)`1 c= G.reachableFrom(the Element of the_Vertices_of G)
proof
let G be _finite real-weighted WGraph;
set src = the Element of the_Vertices_of G;
defpred P[Nat] means (PRIM:CompSeq(G).$1)`1 c=
G.reachableFrom(the Element of
the_Vertices_of G);
set G0 = PRIM:CompSeq(G).0;
G0 = PRIM:Init(G) by Def17;
then
A1: G0`1 = {src};
A2: now
let n be Nat;
assume
A3: P[n];
set Gn = PRIM:CompSeq(G).n, Gn1 = PRIM:CompSeq(G).(n+1);
set Next = PRIM:NextBestEdges(Gn), e = the Element of Next;
set sc = (the_Source_of G).e, tar = (the_Target_of G).e;
A4: Gn1 = PRIM:Step(Gn) by Def17;
now
per cases;
suppose
Next = {};
hence P[n+1] by A3,A4,Def15;
end;
suppose
A5: Next <> {} & sc in Gn`1;
then Gn1 = [Gn`1 \/ {tar}, Gn`2 \/ {e}] by A4,Def15;
then
A6: Gn1`1 = Gn`1 \/ {tar};
A7: e in Next by A5;
now
let v be object;
assume
A8: v in Gn1`1;
now
per cases by A6,A8,XBOOLE_0:def 3;
suppose
v in Gn`1;
hence v in G.reachableFrom(src) by A3;
end;
suppose
v in {tar};
then v = tar by TARSKI:def 1;
then e Joins sc,v,G by A7;
hence v in G.reachableFrom(src) by A3,A5,GLIB_002:10;
end;
end;
hence v in G.reachableFrom(src);
end;
hence P[n+1] by TARSKI:def 3;
end;
suppose
A9: Next <> {} & not sc in Gn`1;
then Gn1 = [Gn`1 \/ {sc}, Gn`2 \/ {e}] by A4,Def15;
then
A10: Gn1`1 = Gn`1 \/ {sc};
A11: e SJoins Gn`1, the_Vertices_of G \ Gn`1, G by A9,Def13;
then
A12: e in the_Edges_of G;
A13: tar in Gn`1 by A9,A11;
now
let v be object;
assume
A14: v in Gn1`1;
now
per cases by A10,A14,XBOOLE_0:def 3;
suppose
v in Gn`1;
hence v in G.reachableFrom(src) by A3;
end;
suppose
v in {sc};
then v = sc by TARSKI:def 1;
then e Joins tar,v,G by A12;
hence v in G.reachableFrom(src) by A3,A13,GLIB_002:10;
end;
end;
hence v in G.reachableFrom(src);
end;
hence P[n+1] by TARSKI:def 3;
end;
end;
hence P[n+1];
end;
src in G.reachableFrom(src) by GLIB_002:9;
then
A15: P[ 0 ] by A1,ZFMISC_1:31;
for n being Nat holds P[n] from NAT_1:sch 2(A15,A2);
hence thesis;
end;
theorem Th34:
for G being _finite real-weighted WGraph, 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
let G be _finite real-weighted WGraph, i,j be Nat;
set PCS = PRIM:CompSeq(G);
set vPCS = (PCS.i)`1, ePCS = (PCS.i)`2;
defpred P[Nat] means vPCS c= (PCS.(i+$1))`1 & ePCS c= (PCS.(i+$1))`2;
assume i <= j;
then
A1: ex x being Nat st j = i + x by NAT_1:10;
now
let k be Nat;
PCS.(i+k+1) = PRIM:Step(PCS.(i+k)) by Def17;
then
A2: (PCS.(i+k))`1 c= (PCS.(i+k+1))`1 & (PCS.(i+k))`2 c= (PCS.(i+k+1))`2 by Th29
;
assume vPCS c= (PCS.(i+k))`1 & ePCS c= (PCS.(i+k))`2;
hence vPCS c= (PCS.(i+(k+1)))`1 & ePCS c= (PCS.(i+(k+1)))`2 by A2;
end;
then
A3: for k being Nat st P[k] holds P[k+1];
A4: P[ 0 ];
for k being Nat holds P[k] from NAT_1:sch 2(A4,A3);
hence thesis by A1;
end;
theorem Th35:
for G being _finite real-weighted WGraph, 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
let G be _finite real-weighted WGraph, n be Nat;
set src = the Element of the_Vertices_of G;
set PCS = PRIM:CompSeq(G), RFS = G.reachableFrom(src);
set Gn = PCS.n;
set EG = the_Edges_of G;
set Next = PRIM:NextBestEdges(Gn);
set GnV = Gn`1, GnVg = the_Vertices_of G \ GnV;
set e = the Element of Next;
hereby
assume
A1: Next = {};
now
defpred P1[set] means $1 SJoins GnV, GnVg, G;
assume
A2: GnV <> RFS;
consider BE1 being Subset of EG such that
A3: for x being set holds x in BE1 iff x in EG & P1[x] from SUBSET_1
:sch 1;
GnV c= RFS by Th33;
then
A4: GnV c< RFS by A2,XBOOLE_0:def 8;
now
src in {src} by TARSKI:def 1;
then src in (PRIM:Init(G))`1;
then
A5: src in (PCS.0)`1 by Def17;
assume
A6: BE1 = {};
consider v being object such that
A7: v in RFS and
A8: not v in Gn`1 by A4,XBOOLE_0:6;
reconsider v as Vertex of G by A7;
consider W being Walk of G such that
A9: W is_Walk_from src, v by A7,GLIB_002:def 5;
defpred P2[Nat] means $1 is odd & $1 <= len W & not W.$1 in GnV;
W.(len W) = W.last() by GLIB_001:def 7
.= v by A9,GLIB_001:def 23;
then
A10: ex k being Nat st P2[k] by A8;
consider k being Nat such that
A11: P2[k] & for m being Nat st P2[m] holds k <= m from NAT_1:sch
5(A10 );
A12: (PCS.0)`1 c= Gn`1 by Th34;
now
per cases;
suppose
k = 1;
then W.k = W.first() by GLIB_001:def 6
.= src by A9,GLIB_001:def 23;
hence contradiction by A5,A12,A11;
end;
suppose
A13: k <> 1;
reconsider k9=k as odd Element of NAT by A11,ORDINAL1:def 12;
1 <= k by A11,ABIAN:12;
then 1 < k by A13,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
then reconsider k2a = k9-2*1 as odd Element of NAT by INT_1:5;
set e = W.(k2a+1);
A14: k - 2 < len W - 0 by A11,XREAL_1:15;
then
A15: e Joins W.k2a, W.(k2a+2),G by GLIB_001:def 3;
then
A16: e in EG;
k2a < k - 0 by XREAL_1:15;
then
A17: W.k2a in GnV by A11,A14;
W.k in the_Vertices_of G by A15,GLIB_000:13;
then W.k in GnVg by A11,XBOOLE_0:def 5;
then P1[e] by A17,A15,GLIB_000:17;
hence contradiction by A3,A6,A16;
end;
end;
hence contradiction;
end;
then reconsider BE1 as non empty finite set;
deffunc F(Element of BE1) = (the_Weight_of G).$1;
consider e1 being Element of BE1 such that
A18: for e2 being Element of BE1 holds F(e1)<=F(e2) from PRE_CIRC:sch 5;
A19: now
let e2 be set;
assume
A20: e2 SJoins GnV, GnVg, G;
reconsider e29 = e2 as Element of BE1 by A3,A20;
(the_Weight_of G).e1 <= (the_Weight_of G).e29 by A18;
hence (the_Weight_of G).e1 <= (the_Weight_of G).e2;
end;
e1 SJoins GnV, GnVg, G by A3;
hence contradiction by A1,A19,Def13;
end;
hence GnV = RFS;
end;
assume
A21: GnV = RFS;
now
assume Next <> {};
then
A22: e SJoins GnV, GnVg, G by Def13;
then
A23: e in EG;
now
per cases by A22;
suppose
A24: (the_Source_of G).e in GnV & (the_Target_of G).e in GnVg;
A25: e Joins (the_Source_of G).e, (the_Target_of G).e, G by A23;
not (the_Target_of G).e in GnV by A24,XBOOLE_0:def 5;
hence contradiction by A21,A24,A25,GLIB_002:10;
end;
suppose
A26: (the_Source_of G).e in GnVg & (the_Target_of G).e in GnV;
A27: e Joins (the_Target_of G).e, (the_Source_of G).e, G by A23;
not (the_Source_of G).e in GnV by A26,XBOOLE_0:def 5;
hence contradiction by A21,A26,A27,GLIB_002:10;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem Th36:
for G being _finite real-weighted WGraph, n being Nat holds card
((PRIM:CompSeq(G).n)`1) = min(n+1,
card(G.reachableFrom(the Element of the_Vertices_of
G)))
proof
let G be _finite real-weighted WGraph;
set CS = PRIM:CompSeq(G), src = the Element of the_Vertices_of G;
defpred P[Nat] means card (PRIM:CompSeq(G).$1)`1 = min($1+1, card(G
.reachableFrom(src)));
set G0 = CS.0;
src in G.reachableFrom(src) by GLIB_002:9;
then {src} c= G.reachableFrom(src) by ZFMISC_1:31;
then card {src} <= card G.reachableFrom(src) by NAT_1:43;
then
A1: 0+1 <= card G.reachableFrom(src) by CARD_1:30;
A2: now
let n be Nat;
assume
A3: P[n];
set Gn = PRIM:CompSeq(G).n, Gn1 = PRIM:CompSeq(G).(n+1);
set e = the Element of PRIM:NextBestEdges(Gn);
A4: Gn1 = PRIM:Step(Gn) by Def17;
now
per cases;
suppose
A5: PRIM:NextBestEdges(Gn) = {};
then
A6: card Gn`1 = card G.reachableFrom(src) by Th35;
then card G.reachableFrom(src) <= n+1 by A3,XXREAL_0:def 9;
then
A7: card G.reachableFrom(src) <= n+1+1 by NAT_1:12;
card Gn1`1 = min(n+1, card (G.reachableFrom(src)) ) by A3,A4,A5,Def15;
hence P[n+1] by A3,A6,A7,XXREAL_0:def 9;
end;
suppose
A8: PRIM:NextBestEdges(Gn) <> {};
A9: Gn`1 c= G.reachableFrom(src) by Th33;
A10: Gn`1 <> G.reachableFrom(src) by A8,Th35;
A11: now
assume
A12: card Gn`1 = card G.reachableFrom(src);
Gn`1 c< G.reachableFrom(src) by A10,A9,XBOOLE_0:def 8;
hence contradiction by A12,CARD_2:48;
end;
then
A13: card Gn`1 = n+1 by A3,XXREAL_0:15;
consider v being Vertex of G such that
A14: not v in Gn`1 and
A15: Gn1 = [Gn`1 \/ {v}, Gn`2 \/ {e}] by A4,A8,Th28;
A16: card Gn1`1 = card (Gn`1 \/ {v}) by A15
.= card Gn`1 + 1 by A14,CARD_2:41;
card Gn`1 <= card G.reachableFrom(src) by Th33,NAT_1:43;
then n+1 < card G.reachableFrom(src) by A11,A13,XXREAL_0:1;
then n+1+1 <= card G.reachableFrom(src) by NAT_1:13;
hence P[n+1] by A16,A13,XXREAL_0:def 9;
end;
end;
hence P[n+1];
end;
G0 = PRIM:Init(G) by Def17;
then {src} = G0`1;
then card G0`1 = 1 by CARD_1:30;
then
A17: P[ 0 ] by A1,XXREAL_0:def 9;
for n being Nat holds P[n] from NAT_1:sch 2(A17,A2);
hence thesis;
end;
theorem Th37:
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)
proof
let G be _finite real-weighted WGraph;
set PCS = PRIM:CompSeq(G);
set src = the Element of the_Vertices_of G, RFS = G.reachableFrom(src);
consider n being Nat such that
A1: n + 1 = card RFS by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
set Gn = PCS.n, Gn1 = PCS.(n+1);
A2: card RFS <= card RFS + 1 by NAT_1:11;
A3: card Gn1`1 = min(card RFS + 1, card RFS) by A1,Th36
.= card RFS by A2,XXREAL_0:def 9;
set e = the Element of PRIM:NextBestEdges(Gn);
A4: card Gn`1 = min(card RFS, card RFS) by A1,Th36
.= card RFS;
A5: Gn1 = PRIM:Step(Gn) by Def17;
then
A6: Gn`1 c= Gn1`1 by Th29;
A7: now
assume Gn`1 <> Gn1`1;
then Gn`1 c< Gn1`1 by A6,XBOOLE_0:def 8;
hence contradiction by A4,A3,CARD_2:48;
end;
now
assume PRIM:NextBestEdges(Gn) <> {};
then consider v being Vertex of G such that
A8: not v in Gn`1 and
A9: Gn1 = [Gn`1 \/ {v}, Gn`2 \/ {e}] by A5,Th28;
A10: v in {v} by TARSKI:def 1;
Gn1`1 = Gn`1 \/ {v} by A9;
hence contradiction by A7,A8,A10,XBOOLE_0:def 3;
end;
then
A11: Gn1 = Gn by A5,Def15;
hence
A12: PCS is halting;
now
let m be Nat;
set Gm = PCS.m;
assume
A13: PCS.m = PCS.(m+1);
now
assume m < n;
then
A14: m+1 <= n by NAT_1:13;
n+0 < card RFS by A1,XREAL_1:8;
then
A15: m+1 < card RFS by A14,XXREAL_0:2;
then
A16: m+1+1 <= card RFS by NAT_1:13;
A17: card Gm`1 = min(m+1, card RFS) by Th36
.= m+1 by A15,XXREAL_0:def 9;
card Gm`1 = min(m+1+1,card RFS) by A13,Th36
.= m+1+1 by A16,XXREAL_0:def 9;
hence contradiction by A17;
end;
hence n <= m;
end;
hence thesis by A1,A11,A12,GLIB_000:def 56;
end;
theorem Th38:
for G1 being _finite real-weighted WGraph, n being Nat, G2 being
inducedSubgraph of G1, (PRIM:CompSeq(G1).n)`1, (PRIM:CompSeq(G1).n)`2 holds G2
is Tree-like
proof
let G1 be _finite real-weighted WGraph;
set PCS = PRIM:CompSeq(G1);
defpred P[Nat] means for G2 being inducedSubgraph of G1,(PCS.$1)`1, (PCS.$1)
`2 holds G2 is Tree-like;
set G0 = PCS.0, src = the Element of the_Vertices_of G1;
now
let n be Nat;
set Gn = PCS.n, Gn1 = PCS.(n+1);
set Next = PRIM:NextBestEdges(Gn), e = the Element of Next;
set G3 = the inducedSubgraph of G1,Gn`1,Gn`2;
A1: Gn1 = PRIM:Step(Gn) by Def17;
A2: Gn`2 c= G1.edgesBetween(Gn`1) by Th30;
Gn`1 is non empty Subset of the_Vertices_of G1 by Th30;
then
A3: the_Vertices_of G3 = Gn`1 & the_Edges_of G3 = Gn`2 by A2,GLIB_000:def 37;
assume
A4: P[n];
then
A5: G3 is Tree-like;
now
A6: G3.order() = G3.size() + 1 by A5,GLIB_002:46;
let G2 be inducedSubgraph of G1,Gn1`1,Gn1`2;
A7: Gn1`2c=G1.edgesBetween(Gn1`1) by Th30;
Gn1`1 is non empty Subset of the_Vertices_of G1 by Th30;
then
A8: the_Vertices_of G2 = Gn1`1 by A7,GLIB_000:def 37;
now
per cases;
suppose
Next = {};
then Gn = Gn1 by A1,Def15;
hence G2 is Tree-like by A4;
end;
suppose
A9: Next <> {};
set GnV = Gn`1, GnVg = the_Vertices_of G1 \ GnV;
A10: e SJoins GnV, GnVg, G1 by A9,Def13;
A11: now
assume
A12: e in Gn`2;
then (the_Target_of G1).e in GnV by A2,GLIB_000:31;
then
A13: not (the_Target_of G1).e in GnVg by XBOOLE_0:def 5;
(the_Source_of G1).e in GnV by A2,A12,GLIB_000:31;
then not (the_Source_of G1).e in GnVg by XBOOLE_0:def 5;
hence contradiction by A10,A13;
end;
consider v being Vertex of G1 such that
A14: not v in Gn`1 and
A15: Gn1 = [Gn`1\/{v},Gn`2\/{e}] by A1,A9,Th28;
A16: card Gn1`1 = card (Gn`1 \/ {v}) by A15
.= card Gn`1 + 1 by A14,CARD_2:41;
card Gn1`2 = card (Gn`2 \/ {e}) by A15
.= card Gn`2 + 1 by A11,CARD_2:41;
then G2.order() = G2.size() + 1 by A3,A7,A8,A6,A16,GLIB_000:def 37;
hence G2 is Tree-like by GLIB_002:47;
end;
end;
hence G2 is Tree-like;
end;
hence P[n+1];
end;
then
A17: for n being Nat st P[n] holds P[n+1];
G0 = PRIM:Init(G1) by Def17;
then G0`1 = {src} & G0`2 = {};
then
A18: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A18,A17);
hence thesis;
end;
theorem Th39:
for G being _finite connected real-weighted WGraph holds (
PRIM:MST(G))`1 = the_Vertices_of G
proof
let G be _finite connected real-weighted WGraph;
set M = PRIM:MST(G), PCS = PRIM:CompSeq(G), V = M`1;
set src = the Element of the_Vertices_of G, RFS = G.reachableFrom(src);
PCS.Lifespan() + 1 = card RFS by Th37;
then
A1: card V = min(card RFS,card RFS) by Th36;
A2: V c= RFS by Th33;
now
assume V <> RFS;
then V c< RFS by A2,XBOOLE_0:def 8;
hence contradiction by A1,CARD_2:48;
end;
hence thesis by GLIB_002:16;
end;
registration
let G be _finite connected real-weighted WGraph;
cluster spanning Tree-like for WSubgraph of G;
existence
proof
set PCS = PRIM:CompSeq(G), n = PCS.Lifespan();
set IT = the inducedWSubgraph of G,(PCS.n)`1,(PCS.n)`2;
take IT;
PRIM:MST(G) = PCS.n;
then
A1: (PCS.n)`1 = the_Vertices_of G by Th39;
thus IT is spanning by A1;
thus thesis by Th38;
end;
end;
definition
let G1 be _finite connected real-weighted WGraph, G2 be spanning Tree-like
WSubgraph of G1;
attr G2 is min-cost means
:Def19:
for G3 being spanning Tree-like WSubgraph of G1 holds G2.cost() <= G3.cost();
end;
registration
let G1 be _finite connected real-weighted WGraph;
cluster min-cost for spanning Tree-like WSubgraph of G1;
existence
proof
set GT = the spanning Tree-like WSubgraph of G1;
set G3 = GT|(WGraphSelectors);
A1: G3 == GT by Lm4;
the_Weight_of G3 = the_Weight_of GT by Lm4;
then reconsider G3 as WSubgraph of G1 by A1,GLIB_003:8;
the_Vertices_of G3 = the_Vertices_of GT by A1
.= the_Vertices_of G1 by GLIB_000:def 33;
then reconsider G3 as spanning Tree-like WSubgraph of G1 by A1,
GLIB_000:def 33,GLIB_002:48;
set X = {G2 where G2 is Element of G1.allWSubgraphs() : G2 is spanning
Tree-like WSubgraph of G1};
now
let x be object;
assume x in X;
then
ex G2 being Element of G1.allWSubgraphs() st x = G2 & G2 is spanning
Tree-like WSubgraph of G1;
hence x in G1.allWSubgraphs();
end;
then reconsider X as finite Subset of G1.allWSubgraphs() by TARSKI:def 3;
deffunc F(_finite real-weighted WGraph) = $1.cost();
dom G3 = WGraphSelectors by Lm5;
then G3 in G1.allWSubgraphs() by Def5;
then G3 in X;
then reconsider X as finite non empty Subset of G1.allWSubgraphs();
consider x being Element of X such that
A2: for y being Element of X holds F(x) <= F(y) from PRE_CIRC:sch 5;
x in X;
then ex G2 being Element of G1.allWSubgraphs() st x = G2 & G2 is spanning
Tree-like WSubgraph of G1;
then reconsider x as spanning Tree-like WSubgraph of G1;
take x;
now
let GT be spanning Tree-like WSubgraph of G1;
set G3 = GT|(WGraphSelectors);
A3: G3 == GT by Lm4;
A4: the_Weight_of G3 = the_Weight_of GT by Lm4;
then reconsider G3 as WSubgraph of G1 by A3,GLIB_003:8;
the_Vertices_of G3 = the_Vertices_of GT by A3
.= the_Vertices_of G1 by GLIB_000:def 33;
then reconsider G3 as spanning Tree-like WSubgraph of G1 by A3,
GLIB_000:def 33,GLIB_002:48;
dom G3 = WGraphSelectors by Lm5;
then G3 in G1.allWSubgraphs() by Def5;
then G3 in X;
then x.cost() <= G3.cost() by A2;
hence x.cost() <= GT.cost() by A3,A4;
end;
hence thesis;
end;
end;
definition
let G be _finite connected real-weighted WGraph;
mode minimumSpanningTree of G is min-cost spanning Tree-like WSubgraph of G;
end;
begin :: Prim's Algorithm Theorems
theorem
for G1,G2 being _finite connected real-weighted WGraph, 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
let G1,G2 be _finite connected real-weighted WGraph, G3 be WSubgraph of G1;
assume that
A1: G3 is minimumSpanningTree of G1 and
A2: G1 == G2 and
A3: the_Weight_of G1 = the_Weight_of G2;
set G39 = G3;
reconsider G39 as Tree-like WSubgraph of G2 by A1,A2,A3,GLIB_003:10;
the_Vertices_of G3 = the_Vertices_of G1 by A1,GLIB_000:def 33
.= the_Vertices_of G2 by A2;
then reconsider G39 as spanning Tree-like WSubgraph of G2 by GLIB_000:def 33;
now
let G be spanning Tree-like WSubgraph of G2;
reconsider G9=G as Tree-like WSubgraph of G1 by A2,A3,GLIB_003:10;
the_Vertices_of G = the_Vertices_of G2 by GLIB_000:def 33
.= the_Vertices_of G1 by A2;
then G9 is spanning;
hence G3.cost() <= G.cost() by A1,Def19;
end;
then G39 is min-cost;
hence thesis;
end;
theorem Th41:
for G being _finite connected real-weighted WGraph, G1 being
minimumSpanningTree of G, G2 being WGraph st G1 == G2 & the_Weight_of G1 =
the_Weight_of G2 holds G2 is minimumSpanningTree of G
proof
let G be _finite connected real-weighted WGraph, G1 be minimumSpanningTree of
G, G2 be WGraph;
assume that
A1: G1 == G2 and
A2: the_Weight_of G1 = the_Weight_of G2;
reconsider G29=G2 as WSubgraph of G by A1,A2,GLIB_003:8;
the_Vertices_of G2 = the_Vertices_of G1 by A1
.= the_Vertices_of G by GLIB_000:def 33;
then reconsider G29 as spanning Tree-like WSubgraph of G by A1,
GLIB_000:def 33,GLIB_002:48;
now
let G3 be spanning Tree-like WSubgraph of G;
G1.cost() <= G3.cost() by Def19;
hence G29.cost() <= G3.cost() by A1,A2;
end;
hence thesis by Def19;
end;
theorem Th42:
for G being _finite connected real-weighted WGraph, n being Nat
holds (PRIM:CompSeq(G).n)`2 c= (PRIM:MST(G))`2
proof
let G be _finite connected real-weighted WGraph, n be Nat;
set PCS = PRIM:CompSeq(G);
defpred P[Nat] means (PCS.(PCS.Lifespan()+$1)) = PRIM:MST(G);
A1: now
set off = PCS.Lifespan();
let n be Nat;
set Gn = PCS.(off+n), Gn1 = PCS.(off+n+1);
set Next = PRIM:NextBestEdges(Gn), e = the Element of Next;
A2: Gn1 = PRIM:Step(Gn) by Def17;
assume
A3: P[n];
then
A4: Gn`1 = the_Vertices_of G by Th39;
now
assume Next <> {};
then
ex v being Vertex of G st ( not v in Gn`1)& Gn1 = [ Gn`1 \/ {v}, Gn`2
\/ {e} ] by A2,Th28;
hence contradiction by A4;
end;
hence P[n+1] by A3,A2,Def15;
end;
A5: P[ 0 ];
A6: for n being Nat holds P[n] from NAT_1:sch 2(A5,A1);
now
per cases;
suppose
n <= PCS.Lifespan();
hence thesis by Th34;
end;
suppose
PCS.Lifespan() < n;
then ex k being Nat st n = PCS.Lifespan() + k by NAT_1:10;
hence thesis by A6;
end;
end;
hence thesis;
end;
::$N Prim's Minimum Spanning Tree Algorithm
::$L https://en.wikipedia.org/wiki/Prim's_algorithm Prim's algorithm
theorem
for G1 being _finite connected real-weighted WGraph, G2 being
inducedWSubgraph of G1, (PRIM:MST(G1))`1, (PRIM:MST(G1))`2 holds G2 is
minimumSpanningTree of G1
proof
let G1 be _finite connected real-weighted WGraph;
set PMST = PRIM:MST(G1);
let G2 be inducedWSubgraph of G1, PMST`1, PMST`2;
reconsider G29=G2 as Tree-like _Graph by Th38;
set VG1 = the_Vertices_of G1, EG1 = the_Edges_of G1;
set WG1 = the_Weight_of G1;
set PCS = PRIM:CompSeq(G1);
A1: PMST`1 = VG1 by Th39;
PMST`2 c= EG1;
then
A2: PMST`2 c= G1.edgesBetween(PMST`1) by A1,GLIB_000:34;
A3: the_Vertices_of G2 = VG1 by A1,A2,GLIB_000:def 37;
A4: the_Edges_of G2 = PMST`2 by A1,A2,GLIB_000:def 37;
A5: G2 is Tree-like by Th38;
now
set X = {x where x is Element of G1.allWSubgraphs() : x is
minimumSpanningTree of G1};
now
let x be object;
assume x in X;
then ex G2 being Element of G1.allWSubgraphs() st x = G2 & G2 is
minimumSpanningTree of G1;
hence x in G1.allWSubgraphs();
end;
then reconsider X as finite Subset of G1.allWSubgraphs() by TARSKI:def 3;
defpred Z[_finite _Graph, Nat] means not (PCS.($2+1))`2 c= the_Edges_of $1
& for n being Nat st n <= $2 holds (PCS.n)`2 c= the_Edges_of $1;
defpred P[_finite _Graph, _finite _Graph] means card (the_Edges_of $1 /\
the_Edges_of G2) > card (the_Edges_of $2 /\ the_Edges_of G2) or (card (
the_Edges_of $1 /\ the_Edges_of G2) = card (the_Edges_of $2 /\ the_Edges_of G2)
& for k1,k2 being Nat st Z[$1,k1] & Z[$2,k2] holds k1 >= k2);
A6: G1.edgesBetween(VG1) = EG1 by GLIB_000:34;
now
set M = the minimumSpanningTree of G1;
set M9 = M|(WGraphSelectors);
M9 == M & the_Weight_of M9 = the_Weight_of M by Lm4;
then reconsider M9 as minimumSpanningTree of G1 by Th41;
dom M9 = WGraphSelectors by Lm5;
then M9 in G1.allWSubgraphs() by Def5;
then M9 in X;
hence X <> {};
end;
then reconsider X as non empty finite Subset of G1.allWSubgraphs();
assume
A7: not G2 is minimumSpanningTree of G1;
A8: now
let G be Element of X;
G in X;
then ex G9 being Element of G1.allWSubgraphs() st G = G9 & G9 is
minimumSpanningTree of G1;
then reconsider G9 = G as minimumSpanningTree of G1;
defpred P4[Nat] means not (PCS.$1)`2c= the_Edges_of G9;
A9: the_Vertices_of G2 = the_Vertices_of G9 by A3,GLIB_000:def 33;
A10: now
assume
A11: the_Edges_of G2 = the_Edges_of G9;
the_Weight_of G2 = (WG1) | the_Edges_of G2 by GLIB_003:def 10
.= the_Weight_of G9 by A11,GLIB_003:def 10;
hence contradiction by A7,A9,A11,Th41,GLIB_000:86;
end;
now
assume the_Edges_of G2 c= the_Edges_of G9;
then the_Edges_of G2 c< the_Edges_of G9 by A10,XBOOLE_0:def 8;
then G2.size() + 1 < G9.size() + 1 by CARD_2:48,XREAL_1:8;
then
A12: G2.order() < G9.size() + 1 by A5,GLIB_002:46;
G2.order() = G9.order() by A3,GLIB_000:def 33;
hence contradiction by A12,GLIB_002:46;
end;
then
A13: ex n being Nat st P4[n] by A4;
consider k3 being Nat such that
A14: P4[k3] & for n being Nat st P4[n] holds k3 <= n from NAT_1:sch
5(A13 );
now
assume k3 = 0;
then
not (PRIM:Init(G1))`2 c= the_Edges_of G9 by A14,Def17;
hence contradiction;
end;
then consider k2 being Nat such that
A16: k2 + 1 = k3 by NAT_1:6;
k2 + 1 - 1 < k3 - 0 by A16,XREAL_1:15;
then
A17: (PCS.k2)`2 c= the_Edges_of G9 by A14;
now
let n be Nat;
assume n <= k2;
then (PCS.n)`2 c= (PCS.k2)`2 by Th34;
hence (PCS.n)`2 c= the_Edges_of G9 by A17;
end;
hence ex k1 being Nat st Z[G,k1] by A14,A16;
end;
now
let x,y,z be Element of X;
assume that
A18: P[x,y] and
A19: P[y,z];
y in X;
then consider y9 being WSubgraph of G1 such that
A20: y9 = y and
dom y9 = WGraphSelectors by Def5;
set CY = card (the_Edges_of y9 /\ the_Edges_of G2);
x in X;
then consider x9 being WSubgraph of G1 such that
A21: x9 = x and
dom x9 = WGraphSelectors by Def5;
z in X;
then consider z9 being WSubgraph of G1 such that
A22: z9 = z and
dom z9 = WGraphSelectors by Def5;
set CZ = card (the_Edges_of z9 /\ the_Edges_of G2);
set CX = card (the_Edges_of x9 /\ the_Edges_of G2);
now
per cases by A18,A21,A20;
suppose
A23: CX > CY;
now
per cases by A19,A20,A22;
suppose
CY > CZ;
hence P[x,z] by A21,A22,A23,XXREAL_0:2;
end;
suppose
CY = CZ & for ky,kz being Nat st Z[y9,ky] & Z[z9,kz]
holds ky >= kz;
hence P[x,z] by A21,A22,A23;
end;
end;
hence P[x,z];
end;
suppose
A24: CX = CY & for kx,ky being Nat st Z[x9,kx] & Z[y9,ky] holds kx >= ky;
now
per cases by A19,A20,A22;
suppose
CY > CZ;
hence P[x,z] by A21,A22,A24;
end;
suppose
A25: CY = CZ & for ky,kz being Nat st Z[y9,ky] & Z[z9,kz]
holds ky >= kz;
consider zy being Nat such that
A26: Z[y,zy] by A8;
now
let kx,kz be Nat;
assume ( Z[x9,kx])& Z[z9,kz];
then kx >= zy & zy >= kz by A20,A24,A25,A26;
hence kx >= kz by XXREAL_0:2;
end;
hence P[x,z] by A21,A22,A24,A25;
end;
end;
hence P[x,z];
end;
end;
hence P[x,z];
end;
then
A27: for x,y,z being Element of X st P[x,y] & P[y,z] holds P[x,z];
A28: now
let G be Element of X, k1,k2 be Nat;
assume
A29: ( Z[G,k1])& Z[G,k2];
then k2+1 > k1;
then
A30: k2 >= k1 by NAT_1:13;
k1+1 > k2 by A29;
then k1 >= k2 by NAT_1:13;
hence k1 = k2 by A30,XXREAL_0:1;
end;
now
let x,y be Element of X;
x in X;
then consider x9 being WSubgraph of G1 such that
A31: x9 = x and
dom x9 = WGraphSelectors by Def5;
set CX = card (the_Edges_of x9 /\ the_Edges_of G2);
y in X;
then consider y9 being WSubgraph of G1 such that
A32: y9 = y and
dom y9 = WGraphSelectors by Def5;
set CY = card (the_Edges_of y9 /\ the_Edges_of G2);
now
per cases by XXREAL_0:1;
suppose
CX < CY;
hence P[x,y] or P[y,x] by A31,A32;
end;
suppose
A33: CY = CX;
consider k1 being Nat such that
A34: Z[x,k1] by A8;
consider k2 being Nat such that
A35: Z[y,k2] by A8;
now
per cases;
suppose
A36: k1 >= k2;
now
let z1,z2 be Nat;
assume that
A37: Z[x,z1] and
A38: Z[y,z2 ];
z1 = k1 by A28,A34,A37;
hence z1 >= z2 by A28,A35,A36,A38;
end;
hence P[x,y] or P[y,x] by A31,A32,A33;
end;
suppose
A39: k1 < k2;
now
let z1,z2 be Nat;
assume that
A40: Z[x,z1] and
A41: Z[y,z2 ];
z1 = k1 by A28,A34,A40;
hence z1 <= z2 by A28,A35,A39,A41;
end;
hence P[x,y] or P[y,x] by A31,A32,A33;
end;
end;
hence P[x,y] or P[y,x];
end;
suppose
CX > CY;
hence P[x,y] or P[y,x] by A31,A32;
end;
end;
hence P[x,y] or P[y,x];
end;
then
A42: for x,y being Element of X holds P[x,y] or P[y,x];
A43: X is finite & X <> {} & X c= X;
consider M being Element of X such that
A44: M in X & for y being Element of X st y in X holds P[M,y] from
CQC_SIM1:sch 4(A43,A42,A27);
ex x being Element of G1.allWSubgraphs() st M = x & x is
minimumSpanningTree of G1 by A44;
then reconsider M as minimumSpanningTree of G1;
defpred P2[Nat] means not (PCS.$1)`2 c= the_Edges_of M;
A45: the_Vertices_of G2 = the_Vertices_of M by A3,GLIB_000:def 33;
A46: now
assume
A47: the_Edges_of G2 = the_Edges_of M;
the_Weight_of G2 = (WG1) | the_Edges_of G2 by GLIB_003:def 10
.= the_Weight_of M by A47,GLIB_003:def 10;
hence contradiction by A7,A45,A47,Th41,GLIB_000:86;
end;
now
assume the_Edges_of G2 c= the_Edges_of M;
then the_Edges_of G2 c< the_Edges_of M by A46,XBOOLE_0:def 8;
then G2.size() + 1 < M.size() + 1 by CARD_2:48,XREAL_1:8;
then
A48: G2.order() < M.size() + 1 by A5,GLIB_002:46;
G2.order() = M.order() by A3,GLIB_000:def 33;
hence contradiction by A48,GLIB_002:46;
end;
then
A49: ex k being Nat st P2[k] by A4;
consider k being Nat such that
A50: P2[k] & for n being Nat st P2[n] holds k <= n from NAT_1:sch 5(
A49);
now
assume k = 0;
then
not (PRIM:Init(G1))`2 c= the_Edges_of M by A50,Def17;
hence contradiction;
end;
then consider k1o being Nat such that
A52: k = k1o + 1 by NAT_1:6;
set Gk1b = PCS.k1o, Gk = PCS.k;
k1o + 1 - 1 < k - 0 by A52,XREAL_1:15;
then
A53: Gk1b`2 c= the_Edges_of M by A50;
set Next = PRIM:NextBestEdges(Gk1b), ep = the Element of Next;
A54: Gk = PRIM:Step(Gk1b) by A52,Def17;
then
A55: Next <> {} by A50,A53,Def15;
then
A56: ep SJoins Gk1b`1, VG1 \ Gk1b`1,G1 by Def13;
ex v being Vertex of G1 st ( not v in Gk1b`1)& Gk = [ Gk1b `1 \/ {v},
Gk1b`2 \/ {ep} ] by A54,A55,Th28;
then
A57: Gk`2 = Gk1b`2 \/ {ep};
then
A58: not {ep} c= the_Edges_of M by A50,A53,XBOOLE_1:8;
then
A59: not ep in the_Edges_of M by ZFMISC_1:31;
set Mep = the inducedWSubgraph of G1,VG1, the_Edges_of M \/ {ep};
A60: ep in Next by A55;
then {ep} c= EG1 by ZFMISC_1:31;
then the_Edges_of M \/ {ep} c= EG1 by XBOOLE_1:8;
then
A61: VG1 c= VG1 & the_Edges_of M \/ {ep} c= G1.edgesBetween(VG1) by GLIB_000:34
;
then
A62: the_Vertices_of Mep = VG1 by GLIB_000:def 37;
VG1 = the_Vertices_of M by GLIB_000:def 33;
then VG1 c= VG1 & M is inducedWSubgraph of G1,VG1, the_Edges_of M by A6,
GLIB_000:def 37;
then
A63: Mep.cost() = M.cost() + (WG1).ep by A60,A59,A6,Th11;
set MG2 = the_Edges_of M /\ the_Edges_of G2;
A64: Gk`2 c= PMST`2 by Th42;
ep in {ep} by TARSKI:def 1;
then
A65: ep in Gk`2 by A57,XBOOLE_0:def 3;
then
A66: {ep} /\ the_Edges_of G2 = {ep} by A4,A64,ZFMISC_1:46;
now
assume MG2 /\ {ep} <> {};
then consider x being object such that
A67: x in MG2 /\ {ep} by XBOOLE_0:def 1;
x in {ep} by A67,XBOOLE_0:def 4;
then
A68: x = ep by TARSKI:def 1;
x in MG2 by A67,XBOOLE_0:def 4;
then x in the_Edges_of M by XBOOLE_0:def 4;
hence contradiction by A58,A68,ZFMISC_1:31;
end;
then
A69: MG2 misses {ep} by XBOOLE_0:def 7;
set v1 = (the_Source_of Mep).ep, v2 = (the_Target_of Mep).ep;
set V = Gk1b`1;
A70: the_Weight_of Mep = (WG1) | the_Edges_of Mep by GLIB_003:def 10;
A71: VG1 = the_Vertices_of M by GLIB_000:def 33;
then reconsider V as non empty Subset of the_Vertices_of M by Th30;
A72: the_Edges_of Mep = the_Edges_of M \/ {ep} by A61,GLIB_000:def 37;
the_Vertices_of M c= the_Vertices_of Mep by A62;
then reconsider M9=M as connected Subgraph of Mep by A72,GLIB_000:44
,XBOOLE_1:7;
ep in {ep} by TARSKI:def 1;
then
A73: ep in the_Edges_of Mep by A72,XBOOLE_0:def 3;
the_Vertices_of Mep = the_Vertices_of M by A62,GLIB_000:def 33;
then reconsider v1,v2 as Vertex of M by A73,FUNCT_2:5;
consider W being Walk of M9 such that
A74: W is_Walk_from v2,v1 by GLIB_002:def 1;
set PW = the Path of W;
reconsider P=PW as Path of Mep by GLIB_001:175;
A75: PW is_Walk_from v2,v1 by A74,GLIB_001:160;
then
A76: P is_Walk_from v2,v1 by GLIB_001:19;
A77: now
reconsider PM = P as Walk of M;
let n be odd Element of NAT;
assume that
A78: 1 < n & n <= len P and
A79: P.n = v2;
v2 = P.first() by A76,GLIB_001:def 23
.= P.(2*0+1) by GLIB_001:def 6;
then n = len P by A78,A79,GLIB_001:def 28;
then P.last() = v2 by A79,GLIB_001:def 7
.= P.first() by A76,GLIB_001:def 23;
then P is closed by GLIB_001:def 24;
then
A80: PM is closed by GLIB_001:176;
PM is non trivial by A78,GLIB_001:126;
then PM is Cycle-like by A80,GLIB_001:def 31;
hence contradiction by GLIB_002:def 2;
end;
A81: ep Joins v1,v2,Mep by A73;
then
A82: ep Joins P.last(),v2,Mep by A76,GLIB_001:def 23;
ep Joins v1,v2,G1 by A81,GLIB_000:72;
then
A83: ep Joins v1,v2,G29 by A4,A65,A64,GLIB_000:73;
v1 <> v2 by A83,GLIB_000:def 18;
then v1 <> P.first() by A76,GLIB_001:def 23;
then P.last() <> P.first() by A76,GLIB_001:def 23;
then
A84: P is open by GLIB_001:def 24;
PW.edges() c= the_Edges_of M;
then P.edges() c= the_Edges_of M by GLIB_001:110;
then not ep in P.edges() by A58,ZFMISC_1:31;
then
A85: P.addEdge(ep) is Path-like by A84,A82,A77,GLIB_001:150;
P.addEdge(ep) is_Walk_from v2,v2 by A76,A81,GLIB_001:66;
then
A86: P.addEdge(ep) is closed by GLIB_001:119;
the_Vertices_of M c= the_Vertices_of Mep by A62;
then reconsider M9=M as connected Subgraph of Mep by A72,GLIB_000:44
,XBOOLE_1:7;
the_Vertices_of M9 = the_Vertices_of Mep by A62,GLIB_000:def 33;
then M9 is spanning;
then
A87: Mep is connected by GLIB_002:23;
A88: v2 = P.1 by A75,GLIB_001:17;
set C = P.addEdge(ep);
A89: v1 = P.(len P) by A75,GLIB_001:17;
A90: (the_Source_of G1).ep = v1 & (the_Target_of G1).ep = v2 by A73,
GLIB_000:def 32;
now
per cases by A56,A90;
suppose
A91: v1 in Gk1b`1 & v2 in VG1\Gk1b`1;
A92: len C = len P + 2 & C.(len P + 1) = ep by A82,GLIB_001:64,65;
defpred P3[Nat] means $1 is odd & $1 <= len P & P.$1 in Gk1b`1;
A93: ex n being Nat st P3[n] by A89,A91;
consider m being Nat such that
A94: P3[m] & for n being Nat st P3[n] holds m <= n from NAT_1:sch
5(A93 );
reconsider m as odd Element of NAT by A94,ORDINAL1:def 12;
1 <= m & m <> 1 by A88,A91,A94,ABIAN:12,XBOOLE_0:def 5;
then 1 < m by XXREAL_0:1;
then 1+1 <= m by NAT_1:13;
then reconsider m2k = m-2*1 as odd Element of NAT by INT_1:5;
A95: m2k < m - 0 by XREAL_1:15;
then
A96: m2k < len P by A94,XXREAL_0:2;
then
A97: not P.m2k in Gk1b`1 by A94,A95;
set em = P.(m2k+1);
A98: em in P.edges() by A96,GLIB_001:100;
then consider i being even Element of NAT such that
A99: 1 <= i and
A100: i <= len P and
A101: P.i = em by GLIB_001:99;
i in dom P by A99,A100,FINSEQ_3:25;
then
A102: C.i = em by A82,A101,GLIB_001:65;
take em;
C.edges() = P.edges() \/ {ep} by A82,GLIB_001:111;
hence em in C.edges() by A98,XBOOLE_0:def 3;
A103: len P + 1 <= len P + 2 by XREAL_1:7;
len P + 0 < len P + 1 by XREAL_1:8;
then i < len P + 1 by A100,XXREAL_0:2;
hence em <> ep by A85,A99,A102,A92,A103,GLIB_001:138;
m2k+2 = m;
then
A104: em Joins PW.m2k, PW.m, M by A96,GLIB_001:def 3;
then PW.m2k in the_Vertices_of M by GLIB_000:13;
then PW.m2k in the_Vertices_of M\Gk1b`1 by A97,XBOOLE_0:def 5;
hence em SJoins V, the_Vertices_of M \ V, M by A94,A104;
end;
suppose
A105: v2 in Gk1b`1 & v1 in VG1\Gk1b `1;
A106: len C = len P + 2 & C.(len P + 1) = ep by A82,GLIB_001:64,65;
defpred P3[Nat] means $1 is odd & $1 <= len P & P.$1 in VG1\Gk1b`1;
A107: ex n being Nat st P3[n] by A89,A105;
consider m being Nat such that
A108: P3[m] & for n being Nat st P3[n] holds m <= n from NAT_1:sch
5(A107);
reconsider m as odd Element of NAT by A108,ORDINAL1:def 12;
1 <= m & m <> 1 by A88,A105,A108,ABIAN:12,XBOOLE_0:def 5;
then 1 < m by XXREAL_0:1;
then 1+1 <= m by NAT_1:13;
then reconsider m2k = m-2*1 as odd Element of NAT by INT_1:5;
A109: m2k < m - 0 by XREAL_1:15;
then
A110: m2k < len P by A108,XXREAL_0:2;
A111: now
assume
A112: not P.m2k in Gk1b`1;
P.m2k in VG1 by A71,A110,GLIB_001:7;
then P.m2k in VG1\Gk1b`1 by A112,XBOOLE_0:def 5;
hence contradiction by A108,A109,A110;
end;
set em = P.(m2k+1);
A113: em in P.edges() by A110,GLIB_001:100;
then consider i being even Element of NAT such that
A114: 1 <= i and
A115: i <= len P and
A116: P.i = em by GLIB_001:99;
i in dom P by A114,A115,FINSEQ_3:25;
then
A117: C.i = em by A82,A116,GLIB_001:65;
take em;
C.edges() = P.edges() \/ {ep} by A82,GLIB_001:111;
hence em in C.edges() by A113,XBOOLE_0:def 3;
A118: len P + 1 <= len P + 2 by XREAL_1:7;
len P + 0 < len P + 1 by XREAL_1:8;
then i < len P + 1 by A115,XXREAL_0:2;
hence em <> ep by A85,A114,A117,A106,A118,GLIB_001:138;
m2k+2 = m;
then em Joins PW.m2k, PW.m, M by A110,GLIB_001:def 3;
hence em SJoins V, the_Vertices_of M \ V, M by A71,A108,A111;
end;
end;
then consider em being set such that
A119: em in C.edges() and
A120: em <> ep and
A121: em SJoins V, the_Vertices_of M \ V, M;
set M2 = the weight-inheriting [Weighted] removeEdge of Mep,em;
reconsider M2 as WSubgraph of G1 by GLIB_003:9;
A122: M2.order() = card VG1 by A62,GLIB_000:53
.= M.order() by GLIB_000:def 33;
A123: em SJoins V, VG1 \ V, G1 by A71,A121,GLIB_000:72;
then
A124: (WG1).ep <= (WG1).em by A55,Def13;
set M29 = M2|(WGraphSelectors);
A125: M29 == M2 by Lm4;
A126: the_Edges_of M2 = the_Edges_of M \/ {ep} \{em} by A72,GLIB_000:51;
then
A127: the_Edges_of M29 = the_Edges_of M \/ {ep} \ {em} by A125;
{em} c= the_Edges_of M \/ {ep} by A72,A119,ZFMISC_1:31;
then M2.size() = card (the_Edges_of M \/{ep})-card {em} by A126,CARD_2:44
.= card (the_Edges_of M \/ {ep}) - 1 by CARD_1:30
.= card the_Edges_of M + 1 - 1 by A59,CARD_2:41
.= M.size();
then
A128: M2.order() = M2.size() + 1 by A122,GLIB_002:46;
A129: the_Weight_of M29 = the_Weight_of M2 by Lm4;
then reconsider M29 as WSubgraph of G1 by A125,GLIB_003:8;
A130: the_Vertices_of M29 = the_Vertices_of M2 by A125
.= VG1 by A62,GLIB_000:53;
P.addEdge(ep) is non trivial by A82,GLIB_001:132;
then C is Cycle-like by A85,A86,GLIB_001:def 31;
then M2 is connected by A119,A87,GLIB_002:5;
then M2 is Tree-like by A128,GLIB_002:47;
then M29 is Tree-like by Lm4,GLIB_002:48;
then reconsider M29 as spanning Tree-like WSubgraph of G1 by A130,
GLIB_000:def 33;
M2.cost() + (the_Weight_of Mep).em = Mep.cost() by A119,Th10;
then M2.cost() = Mep.cost() - (the_Weight_of Mep).em;
then M2.cost() = M.cost()+(WG1).ep-(WG1).em by A119,A63,A70,FUNCT_1:49;
then M29.cost() = M.cost()+(WG1).ep - (WG1).em by A125,A129;
then
A131: M29.cost() + (WG1).em - (WG1).em <= M.cost() + (WG1).ep - (WG1).ep
by A124,XREAL_1:13;
now
let G3 being spanning Tree-like WSubgraph of G1;
M.cost() <= G3.cost() by Def19;
hence M29.cost() <= G3.cost() by A131,XXREAL_0:2;
end;
then reconsider M29 as minimumSpanningTree of G1 by Def19;
set MG29 = the_Edges_of M29 /\ the_Edges_of G2;
A132: MG29 = ((the_Edges_of M \/ {ep}) /\ the_Edges_of G2) \ {em} /\
the_Edges_of G2 by A127,XBOOLE_1:50;
dom M29 = WGraphSelectors by Lm5;
then M29 in G1.allWSubgraphs() by Def5;
then
A133: M29 in X;
A134: now
thus not (PCS.(k1o+1))`2 c= the_Edges_of M by A50,A52;
let n be Nat;
assume n <= k1o;
then (PCS.n)`2 c= Gk1b`2 by Th34;
hence (PCS.n)`2 c= the_Edges_of M by A53;
end;
A135: now
consider k2 being Nat such that
A136: Z[M29,k2] by A8,A133;
A137: now
set Vr = VG1 \ V;
assume
A138: em in Gk1b`2;
A139: Gk1b`2 c= G1.edgesBetween(Gk1b`1) by Th30;
then (the_Target_of G1).em in Gk1b`1 by A138,GLIB_000:31;
then
A140: not (the_Target_of G1).em in Vr by XBOOLE_0:def 5;
(the_Source_of G1).em in Gk1b`1 by A138,A139,GLIB_000:31;
then not (the_Source_of G1).em in Vr by XBOOLE_0:def 5;
hence contradiction by A123,A140;
end;
now
let x be object;
assume
A141: x in Gk`2;
now
per cases by A57,A141,XBOOLE_0:def 3;
suppose
x in Gk1b`2;
then x in the_Edges_of M \/ {ep} & not x in {em} by A53,A137,
TARSKI:def 1,XBOOLE_0:def 3;
hence x in the_Edges_of M29 by A127,XBOOLE_0:def 5;
end;
suppose
A142: x in {ep};
then x = ep by TARSKI:def 1;
then
A143: not x in {em} by A120,TARSKI:def 1;
x in the_Edges_of M \/ {ep} by A142,XBOOLE_0:def 3;
hence x in the_Edges_of M29 by A127,A143,XBOOLE_0:def 5;
end;
end;
hence x in the_Edges_of M29;
end;
then
A144: Gk`2 c= the_Edges_of M29;
A145: now
assume k2 < k;
then k2+1 <= k by NAT_1:13;
then (PCS.(k2+1))`2 c= Gk`2 by Th34;
hence contradiction by A136,A144,XBOOLE_1:1;
end;
assume
A146: em in the_Edges_of G2;
now
let x be object;
assume x in {em};
then x = em by TARSKI:def 1;
hence x in (the_Edges_of M \/ {ep}) /\ the_Edges_of G2 by A72,A119,A146
,XBOOLE_0:def 4;
end;
then
A147: {em}c=(the_Edges_of M\/{ep})/\the_Edges_of G2;
MG29=((the_Edges_of M\/{ep})/\the_Edges_of G2)\{em} by A132,A146,
ZFMISC_1:46;
then card MG29 = card (the_Edges_of Mep /\ the_Edges_of G2) - card {em}
by A72,A147,CARD_2:44
.= card (the_Edges_of Mep /\ the_Edges_of G2) - 1 by CARD_1:30
.= card (MG2 \/ {ep}) - 1 by A72,A66,XBOOLE_1:23
.= card MG2 + card {ep} - 1 by A69,CARD_2:40
.= card MG2 + 1 - 1 by CARD_1:30
.= card MG2;
then
A148: k1o >= k2 by A44,A133,A134,A136;
k1o + 1 - 1 < k - 0 by A52,XREAL_1:15;
hence contradiction by A145,A148,XXREAL_0:2;
end;
now
assume {em} /\ the_Edges_of G2 <> {};
then consider x being object such that
A149: x in {em} /\ the_Edges_of G2 by XBOOLE_0:def 1;
x in {em} & x in the_Edges_of G2 by A149,XBOOLE_0:def 4;
hence contradiction by A135,TARSKI:def 1;
end;
then
A150: MG29 = MG2 \/ ({ep} /\ the_Edges_of G2) by A132,XBOOLE_1:23;
now
assume MG2 /\ {ep} <> {};
then consider x being object such that
A151: x in MG2 /\ {ep} by XBOOLE_0:def 1;
x in {ep} by A151,XBOOLE_0:def 4;
then
A152: x = ep by TARSKI:def 1;
x in MG2 by A151,XBOOLE_0:def 4;
then x in the_Edges_of M by XBOOLE_0:def 4;
hence contradiction by A58,A152,ZFMISC_1:31;
end;
then MG2 misses {ep} by XBOOLE_0:def 7;
then card MG29 = card MG2 + card {ep} by A66,A150,CARD_2:40
.= card MG2 + 1 by CARD_1:30;
then card MG2 + 0 >= card MG2 + 1 by A44,A133;
hence contradiction by XREAL_1:6;
end;
hence thesis;
end;