:: Dijkstra's Shortest Path Algorithm
:: by Jing-Chao Chen
::
:: Received March 17, 2003
:: Copyright (c) 2003-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, SUBSET_1, FINSEQ_1, INT_1, RELAT_1, FUNCT_1, ORDINAL4,
XBOOLE_0, XXREAL_0, PARTFUN1, GRAPH_1, STRUCT_0, TREES_2, GLIB_000,
GRAPH_5, CARD_3, GRAPH_4, NAT_1, ARYTM_3, TARSKI, CARD_1, FINSET_1,
FUNCT_4, REAL_1, FUNCT_2, ARYTM_1, GRAPHSP, XREAL_0;
notations XCMPLX_0, XXREAL_0, REAL_1, INT_1, TARSKI, XBOOLE_0, SUBSET_1,
RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1,
ORDINAL1, XREAL_0, STRUCT_0, GRAPH_1, PARTFUN1, FUNCT_2, CQC_SIM1,
GRAPH_4, GRAPH_5, NAT_D, DOMAIN_1, RVSUM_1, NUMBERS, FUNCT_7, NAT_1;
constructors DOMAIN_1, REAL_1, FINSEQ_4, FINSOP_1, NAT_D, FUNCT_7, CQC_SIM1,
GRAPH_4, GRAPH_5, BINOP_2, RVSUM_1, RELSET_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, GRAPH_1, GRAPH_4, GRAPH_5,
VALUED_0, CARD_1, FUNCT_1, XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI;
equalities RVSUM_1;
expansions TARSKI;
theorems FUNCT_2, FUNCT_1, PARTFUN1, FINSEQ_1, NAT_1, ZFMISC_1, TARSKI,
FINSEQ_3, XBOOLE_0, XBOOLE_1, SUBSET_1, GRAPH_1, FINSEQ_4, CARD_2, INT_1,
GRAPH_5, GRAPH_4, FINSEQ_2, ENUMSET1, FUNCT_7, XREAL_1, XXREAL_0,
FINSOP_1, ORDINAL1, NAT_D, XREAL_0;
schemes NAT_1, CLASSES1, PRE_CIRC;
begin :: Preliminaries
reserve x,y,X for set,
i,j,k,m,n for Nat,
p for FinSequence of X,
ii for Integer;
theorem Th1:
for p being FinSequence,x being set holds not x in rng p & p is
one-to-one iff p^<*x*> is one-to-one
proof
let p be FinSequence,x be set;
A1: rng <*x*> = {x} by FINSEQ_1:38;
rng p misses rng <*x*> & p is one-to-one & <*x*> is one-to-one iff p ^
<*x*> is one-to-one by FINSEQ_3:91;
hence thesis by A1,FINSEQ_3:93,ZFMISC_1:48,50;
end;
theorem Th2:
1 <= ii & ii <= len p implies p.ii in X
proof
assume that
A1: 1 <= ii and
A2: ii <= len p;
reconsider ii as Element of NAT by A1,INT_1:3;
ii in dom p by A1,A2,FINSEQ_3:25;
hence thesis by PARTFUN1:4;
end;
theorem Th3:
1 <= ii & ii <= len p implies p/.ii = p.ii
proof
assume that
A1: 1 <= ii and
A2: ii <= len p;
reconsider ii as Element of NAT by A1,INT_1:3;
ii in dom p by A1,A2,FINSEQ_3:25;
hence thesis by PARTFUN1:def 6;
end;
reserve G for Graph,
pe,qe for FinSequence of the carrier' of G,
p,q for oriented Chain of G,
W for Function,
U,V,e,ee for set,
v1,v2,v3,v4 for Vertex of G;
theorem Th4:
W is_weight_of G & len pe = 1 implies cost(pe,W) = W.(pe.1)
proof
assume that
A1: W is_weight_of G and
A2: len pe = 1;
A3: 1 in dom pe by A2,FINSEQ_3:25;
set f=RealSequence(pe,W);
reconsider f1 = f.1 as Element of REAL by XREAL_0:def 1;
dom f = dom pe by A1,GRAPH_5:def 15;
then len f=1 by A2,FINSEQ_3:29;
then
A4: f = <*f1*> by FINSEQ_1:40;
thus cost(pe,W) = Sum f by GRAPH_5:def 16
.= f.1 by A4,FINSOP_1:11
.= W.(pe.1) by A1,A3,GRAPH_5:def 15;
end;
theorem Th5:
e in the carrier' of G implies <*e*> is Simple oriented Chain of G
proof
assume e in the carrier' of G;
then
A1: <*e*> is FinSequence of the carrier' of G by FINSEQ_1:74;
len <*e*> = 1 by FINSEQ_1:40;
hence thesis by A1,GRAPH_5:15;
end;
Lm1: for n be Nat for p,q being FinSequence st 1 <= n & n <= len p
holds p.n = (p^q).n
proof
let n be Nat;
let p,q be FinSequence;
assume 1 <= n & n <= len p;
then n in dom p by FINSEQ_3:25;
hence thesis by FINSEQ_1:def 7;
end;
Lm2: for p,q being FinSequence st 1 <= n & n <= len q holds q.n = (p^q).(len p
+n)
proof
let p,q be FinSequence;
assume 1 <= n & n <= len q;
then n in dom q by FINSEQ_3:25;
hence thesis by FINSEQ_1:def 7;
end;
theorem Th6:
for p being Simple oriented Chain of G st p=pe^qe & len pe >= 1
& len qe >= 1 holds (the Target of G).(p.len p) <> (the Target of G).(pe.len pe
) & (the Source of G).(p.1) <> (the Source of G).(qe.1)
proof
let p be Simple oriented Chain of G;
set FT=the Target of G, FS=the Source of G;
assume that
A1: p=pe^qe and
A2: len pe >= 1 and
A3: len qe >= 1;
consider vs being FinSequence of the carrier of G such that
A4: vs is_oriented_vertex_seq_of p and
A5: for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
by GRAPH_4:def 7;
A6: len vs = len p + 1 by A4,GRAPH_4:def 5;
then
A7: 1 <= len vs by NAT_1:12;
len p = len pe + len qe by A1,FINSEQ_1:22;
then
A8: len p >= len pe+1 by A3,XREAL_1:7;
then
A9: len pe+1 < len vs by A6,NAT_1:13;
A10: len p > len pe by A8,NAT_1:13;
then
A11: len p >= 1 by A2,XXREAL_0:2;
then p.1 orientedly_joins vs/.1, vs/.(1+1) by A4,GRAPH_4:def 5;
then
A12: FS.(p.1)=vs/.1 by GRAPH_4:def 1
.=vs.1 by A7,FINSEQ_4:15;
A13: p.len pe orientedly_joins vs/.len pe, vs/.(len pe+1) by A2,A4,A10,
GRAPH_4:def 5;
p.len p orientedly_joins vs/.len p, vs/.(len p+1) by A4,A11,GRAPH_4:def 5;
then
A14: FT.(p.len p)=vs/.(len p+1) by GRAPH_4:def 1
.=vs.len vs by A6,A7,FINSEQ_4:15;
A15: 1 < len pe +1 by A2,NAT_1:13;
then
A16: p.(len pe+1) orientedly_joins vs/.(len pe+1), vs/.(len pe+1+1) by A4,A8,
GRAPH_4:def 5;
FT.(pe.len pe) = FT.(p.len pe) by A1,A2,Lm1
.=vs/.(len pe+1) by A13,GRAPH_4:def 1
.=vs.(len pe +1) by A15,A9,FINSEQ_4:15;
hence FT.(p.len p) <> FT.(pe.len pe) by A5,A14,A15,A9;
assume
A17: FS.(p.1) = FS.(qe.1);
FS.(qe.1) = FS.(p.(len pe+1)) by A1,A3,Lm2
.=vs/.(len pe+1) by A16,GRAPH_4:def 1
.=vs.(len pe +1) by A15,A9,FINSEQ_4:15;
hence contradiction by A5,A15,A9,A12,A17;
end;
begin :: The fundamental properties of directed paths and shortest paths
theorem Th7:
p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2}
proof
set V9=V \/ {v2};
thus p is_orientedpath_of v1,v2,V implies p is_orientedpath_of v1,v2,V9 by
GRAPH_5:32,XBOOLE_1:7;
assume
A1: p is_orientedpath_of v1,v2,V9;
then vertices(p) \ {v2} c= V9 by GRAPH_5:def 4;
then vertices(p) \ {v2} \ {v2} c= V by XBOOLE_1:43;
then
A2: vertices(p) \ ({v2} \/ {v2}) c= V by XBOOLE_1:41;
p is_orientedpath_of v1,v2 by A1,GRAPH_5:def 4;
hence thesis by A2,GRAPH_5:def 4;
end;
theorem Th8:
p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/{v2},W
proof
set V9=V \/ {v2};
hereby
assume
A1: p is_shortestpath_of v1,v2,V,W;
A2: now
let q;
assume q is_orientedpath_of v1,v2,V9;
then q is_orientedpath_of v1,v2,V by Th7;
hence cost(p,W) <= cost(q,W) by A1,GRAPH_5:def 18;
end;
p is_orientedpath_of v1,v2,V by A1,GRAPH_5:def 18;
then p is_orientedpath_of v1,v2,V9 by Th7;
hence p is_shortestpath_of v1,v2,V9,W by A2,GRAPH_5:def 18;
end;
assume
A3: p is_shortestpath_of v1,v2,V9,W;
A4: now
let q;
assume q is_orientedpath_of v1,v2,V;
then q is_orientedpath_of v1,v2,V9 by Th7;
hence cost(p,W) <= cost(q,W) by A3,GRAPH_5:def 18;
end;
p is_orientedpath_of v1,v2,V9 by A3,GRAPH_5:def 18;
then p is_orientedpath_of v1,v2,V by Th7;
hence thesis by A4,GRAPH_5:def 18;
end;
theorem Th9:
p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W
implies cost(p,W)=cost(q,W)
proof
assume that
A1: p is_shortestpath_of v1,v2,V,W and
A2: q is_shortestpath_of v1,v2,V,W;
q is_orientedpath_of v1,v2,V by A2,GRAPH_5:def 18;
then
A3: cost(p,W) <= cost(q,W) by A1,GRAPH_5:def 18;
p is_orientedpath_of v1,v2,V by A1,GRAPH_5:def 18;
then cost(q,W) <= cost(p,W) by A2,GRAPH_5:def 18;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th10:
for G being oriented Graph,v1,v2 be Vertex of G,e1,e2 be set st
e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 &
e2 orientedly_joins v1,v2 holds e1=e2
proof
let G be oriented Graph,v1,v2 be Vertex of G,e1,e2 be set;
assume that
A1: e1 in the carrier' of G & e2 in the carrier' of G and
A2: e1 orientedly_joins v1,v2 and
A3: e2 orientedly_joins v1,v2;
A4: (the Source of G).e2 = v1 & (the Target of G).e2 = v2 by A3,GRAPH_4:def 1;
(the Source of G).e1 = v1 & (the Target of G).e1 = v2 by A2,GRAPH_4:def 1;
hence thesis by A1,A4,GRAPH_1:def 7;
end;
Lm3: 1 <= i & i <= len pe implies (the Source of G).(pe.i) in the carrier of G
& (the Target of G).(pe.i) in the carrier of G
proof
assume 1 <= i & i <= len pe;
then i in dom pe by FINSEQ_3:25;
hence thesis by GRAPH_5:8;
end;
theorem Th11:
the carrier of G= U \/ V & v1 in U & v2 in V & (for v3,v4 st v3
in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins
v3,v4)) implies not ex p st p is_orientedpath_of v1,v2
proof
assume that
A1: the carrier of G= U \/ V and
A2: v1 in U and
A3: v2 in V and
A4: for v3,v4 st v3 in U & v4 in V holds not (ex e st e in the carrier'
of G & e orientedly_joins v3,v4);
set FS=the Source of G, FT=the Target of G;
given p such that
A5: p is_orientedpath_of v1,v2;
p <> {} by A5,GRAPH_5:def 3;
then
A6: len p >= 1 by FINSEQ_1:20;
defpred PP[Nat] means $1 >=1 & $1<=len p & FS.(p.$1) in U;
A7: for k be Nat st PP[k] holds k <= len p;
FS.(p.1) = v1 by A5,GRAPH_5:def 3;
then
A8: ex k be Nat st PP[k] by A2,A6;
consider k be Nat such that
A9: PP[k] & for n be Nat st PP[n] holds n <= k from NAT_1:sch 6(A7,A8
);
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider vx=FS.(p.k) as Vertex of G by A9,Lm3;
A10: p.k in the carrier' of G by A9,Th2;
A11: FT.(p.(len p))= v2 by A5,GRAPH_5:def 3;
per cases;
suppose
k=len p;
then p.k orientedly_joins vx,v2 by A11,GRAPH_4:def 1;
hence contradiction by A3,A4,A9,A10;
end;
suppose
k<>len p;
then
A12: k < len p by A9,XXREAL_0:1;
A13: k < k+1 by NAT_1:13;
A14: now
assume
A15: FS.(p.(k+1)) in U;
k+1 <= len p & 1 <= k+1 by A12,INT_1:7,NAT_1:12;
hence contradiction by A9,A13,A15;
end;
reconsider vy=FT.(p.k) as Vertex of G by A9,Lm3;
A16: p.k orientedly_joins vx,vy by GRAPH_4:def 1;
FS.(p.(k+1)) = FT.(p.k) by A9,A12,GRAPH_1:def 15;
then vy in V by A1,A2,A14,XBOOLE_0:def 3;
hence contradiction by A4,A9,A10,A16;
end;
end;
Lm4: 1<= i & i <= len pe & (v1=(the Source of G).(pe.i) or v1=(the Target of G
).(pe.i)) implies v1 in vertices pe
proof
assume that
A1: 1<= i & i <= len pe and
A2: v1=(the Source of G).(pe.i) or v1=(the Target of G).(pe.i);
i in dom pe by A1,FINSEQ_3:25;
hence thesis by A2,GRAPH_5:24;
end;
theorem Th12:
the carrier of G= U \/ V & v1 in U & (for v3,v4 st v3 in U & v4
in V holds not (ex e st e in the carrier' of G & e orientedly_joins v3,v4)) & p
is_orientedpath_of v1,v2 implies p is_orientedpath_of v1,v2,U
proof
assume that
A1: the carrier of G= U \/ V and
A2: v1 in U and
A3: for v3,v4 st v3 in U & v4 in V holds not (ex e st e in the carrier'
of G & e orientedly_joins v3,v4) and
A4: p is_orientedpath_of v1,v2;
set FS=the Source of G, FT=the Target of G;
A5: now
assume not vertices p c= U;
then consider
i being Element of NAT, q,r being FinSequence of the carrier' of
G such that
A6: i+1 <= len p and
A7: not vertices(p/.(i+1)) c= U and
A8: len q=i and
A9: p=q^r and
A10: vertices q c= U by GRAPH_5:20;
A11: p.(i+1) in the carrier' of G by A6,Th2,NAT_1:12;
p/.(i+1)=p.(i+1) by A6,FINSEQ_4:15,NAT_1:12;
then
A12: vertices(p/.(i+1))={FS.(p.(i+1)),FT.(p.(i+1))} by GRAPH_5:def 1;
A13: now
assume FS.(p.(i+1)) in U & FT.(p.(i+1)) in U;
then vertices(p/.(i+1)) \/ U = U by A12,ZFMISC_1:42;
hence contradiction by A7,XBOOLE_1:7;
end;
A14: 1 <= i+ 1 by NAT_1:12;
then reconsider vy=FT.(p.(i+1)) as Vertex of G by A6,Lm3;
A15: vy in U or vy in V by A1,A2,XBOOLE_0:def 3;
per cases;
suppose
A16: i=0;
then FS.(p.(i+1))=v1 by A4,GRAPH_5:def 3;
then p.(i+1) orientedly_joins v1,vy by GRAPH_4:def 1;
hence contradiction by A2,A3,A4,A13,A11,A15,A16,GRAPH_5:def 3;
end;
suppose
A17: i<>0;
reconsider vx=FS.(p.(i+1)) as Vertex of G by A6,A14,Lm3;
hereby
per cases;
suppose
A18: vx in U;
p.(i+1) orientedly_joins vx,vy by GRAPH_4:def 1;
hence contradiction by A3,A6,A14,A13,A15,A18,Th2;
end;
suppose
A19: not vx in U;
A20: i < len p by A6,NAT_1:13;
A21: i >= 1+0 by A17,INT_1:7;
then reconsider vq=FT.(q.i) as Vertex of G by A8,Lm3;
A22: vq in vertices(q) by A8,A21,Lm4;
FT.(q.i)=FT.(p.i) by A8,A9,A21,Lm1
.=FS.(p.(i+1)) by A21,A20,GRAPH_1:def 15;
hence contradiction by A10,A19,A22;
end;
end;
end;
end;
vertices p \ {v2} c= vertices p by XBOOLE_1:36;
then vertices(p) \ {v2} c= U by A5;
hence thesis by A4,GRAPH_5:def 4;
end;
begin :: The basic theorems for Dijkstra's shortest path algorithm (continue)
reserve G for finite Graph,
P,Q for oriented Chain of G,
v1,v2,v3 for Vertex of G;
theorem Th13:
W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 &
v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & not (ex e st e in the carrier' of G
& e orientedly_joins v2,v3) & P islongestInShortestpath V,v1,W implies Q
is_shortestpath_of v1,v3,V \/{v2},W
proof
assume that
A1: W is_weight>=0of G and
A2: P is_shortestpath_of v1,v2,V,W and
A3: v1 <> v2 and
A4: v1 <> v3 and
A5: Q is_shortestpath_of v1,v3,V,W and
A6: not(ex e st e in the carrier' of G & e orientedly_joins v2,v3) and
A7: P islongestInShortestpath V,v1,W;
set V9=V \/ {v2}, FS=the Source of G, FT=the Target of G;
A8: now
let S be oriented Chain of G;
assume
A9: S is_orientedpath_of v1,v3,V9;
then consider s being Simple oriented Chain of G such that
A10: s is_shortestpath_of v1,v3,V9,W by A1,GRAPH_5:62;
A11: cost(s,W) <= cost(S,W) by A9,A10,GRAPH_5:def 18;
A12: s is_orientedpath_of v1,v3,V9 by A10,GRAPH_5:def 18;
then
A13: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;
then
A14: FS.(s.1)=v1 by GRAPH_5:def 3;
s <> {} by A13,GRAPH_5:def 3;
then len s >=1 by FINSEQ_1:20;
then consider i being Nat such that
A15: len s = 1+i by NAT_1:10;
A16: vertices(s) \ {v3} c= V9 by A12,GRAPH_5:def 4;
A17: FT.(s.len s)=v3 by A13,GRAPH_5:def 3;
consider s1,s2 being FinSequence such that
A18: len s1 = i and
A19: len s2 = 1 and
A20: s = s1^s2 by A15,FINSEQ_2:22;
reconsider s1,s2 as Simple oriented Chain of G by A20,GRAPH_5:14;
reconsider vx=FS.(s2.1) as Vertex of G by A19,Lm3;
A21: s2.1= s.len s by A15,A18,A19,A20,Lm2;
A22: now
assume vx=v2;
then
A23: s2.1 orientedly_joins v2,v3 by A21,A17,GRAPH_4:def 1;
1 in dom s2 by A19,FINSEQ_3:25;
hence contradiction by A6,A23,FINSEQ_2:11;
end;
per cases;
suppose
A24: not v2 in vertices s or v2=v3;
set Vs=vertices s;
(Vs \ {v3}) \ {v2} c= V by A16,XBOOLE_1:43;
then
A25: Vs \ ({v3} \/ {v2}) c= V by XBOOLE_1:41;
now
per cases by A24;
suppose
A26: not v2 in vertices s;
(Vs \ {v2}) \ {v3} c= V by A25,XBOOLE_1:41;
hence Vs \ {v3} c= V by A26,ZFMISC_1:57;
end;
suppose
v2=v3;
hence Vs \ {v3} c= V by A25;
end;
end;
then s is_orientedpath_of v1,v3,V by A13,GRAPH_5:def 4;
then cost(Q,W) <= cost(s,W) by A5,GRAPH_5:def 18;
hence cost(Q,W) <= cost(S,W) by A11,XXREAL_0:2;
end;
suppose
A27: v2 in vertices s & v2<>v3;
A28: len s1 < len s by A15,A18,NAT_1:13;
consider j such that
A29: 1<=j and
A30: j <= len s and
A31: v2 = FT.(s.j) by A3,A14,A27,GRAPH_5:28;
len s1 <> 0 by A15,A18,A17,A27,A29,A30,A31,XXREAL_0:1;
then
A32: len s1 >= 0+1 by INT_1:7;
vx=FS.(s.(len s1+1)) by A19,A20,Lm2
.=FT.(s.len s1) by A32,A28,GRAPH_1:def 15;
then vx = FT.(s1.len s1) by A20,A32,Lm1;
then
A33: vx in vertices(s1) by A32,Lm4;
not vx in {v2} by A22,TARSKI:def 1;
then
A34: vx in (vertices(s1) \ {v2}) by A33,XBOOLE_0:def 5;
A35: now
assume j > len s1;
then j >= len s1+1 by INT_1:7;
hence contradiction by A15,A18,A17,A27,A30,A31,XXREAL_0:1;
end;
then consider k being Nat such that
A36: len s1 = j+k by NAT_1:10;
consider t1,t2 being FinSequence such that
A37: len t1 = j and
len t2 = k and
A38: s1 = t1^t2 by A36,FINSEQ_2:22;
reconsider t1,t2 as Simple oriented Chain of G by A38,GRAPH_5:14;
A39: t1 <> {} by A29,A37;
set Vt=vertices(t1);
vertices(s1^s2) \ {v3} c= V9 by A12,A20,GRAPH_5:def 4;
then
A40: vertices(t1^t2) \ {v3} c= V9 by A38,GRAPH_5:23;
then
A41: Vt \ {v3} c= V9 by GRAPH_5:23;
A42: len s2>=1 by A19;
then not v3 in vertices (s1) by A4,A20,A14,A17,A32,GRAPH_5:18;
then vertices(s1) c= V9 by A38,A40,ZFMISC_1:57;
then
A43: vertices(s1) \ {v2} c= V by XBOOLE_1:43;
not v1 in vertices (s2) by A4,A19,A20,A14,A17,A32,GRAPH_5:18;
then vx <> v1 by A19,Lm4;
then consider q being oriented Chain of G such that
A44: q is_shortestpath_of v1,vx,V,W and
A45: cost(q,W) <= cost(P,W) by A7,A34,A43,GRAPH_5:def 19;
A46: 0 <= cost(t2,W) by A1,GRAPH_5:50;
Vt c= vertices (t1^t2) by GRAPH_5:26;
then not v3 in Vt by A4,A20,A14,A17,A32,A38,A42,GRAPH_5:18;
then Vt c= V9 by A41,ZFMISC_1:57;
then
A47: Vt \ {v2} c= V by XBOOLE_1:43;
A48: FS.(t1.1)=FS.(s1.1) by A29,A37,A38,Lm1
.=v1 by A20,A14,A32,Lm1;
cost(s1,W) = cost(t1,W)+cost(t2,W) by A1,A38,GRAPH_5:46,54;
then
A49: 0+cost(t1,W) <= cost(s1,W) by A46,XREAL_1:7;
FT.(t1.len t1)=FT.(s1.j) by A29,A37,A38,Lm1
.=v2 by A20,A29,A31,A35,Lm1;
then t1 is_orientedpath_of v1,v2 by A48,A39,GRAPH_5:def 3;
then t1 is_orientedpath_of v1,v2,V by A47,GRAPH_5:def 4;
then cost(P,W) <= cost(t1,W) by A2,GRAPH_5:def 18;
then cost(q,W) <= cost(t1,W) by A45,XXREAL_0:2;
then
A50: cost(q,W) <= cost(s1,W) by A49,XXREAL_0:2;
A51: s2.1 orientedly_joins vx,v3 by A21,A17,GRAPH_4:def 1;
A52: q is_orientedpath_of v1,vx,V by A44,GRAPH_5:def 18;
then
A53: q is_orientedpath_of v1,vx by GRAPH_5:def 4;
then q <> {} by GRAPH_5:def 3;
then
A54: len q >=1 by FINSEQ_1:20;
then consider p being oriented Chain of G such that
A55: p=q^s2 and
p is_orientedpath_of v1,v3 by A19,A51,A53,GRAPH_5:33;
p is_orientedpath_of v1,v3,V \/{vx} by A19,A52,A51,A54,A55,GRAPH_5:34;
then p is_orientedpath_of v1,v3,V by A34,A43,ZFMISC_1:40;
then cost(Q,W) <= cost(p,W) by A5,GRAPH_5:def 18;
then
A56: cost(Q,W) <= cost(q,W)+cost(s2,W) by A1,A55,GRAPH_5:46,54;
cost(s,W) = cost(s1,W)+cost(s2,W) by A1,A20,GRAPH_5:46,54;
then cost(q,W)+cost(s2,W) <= cost(s,W) by A50,XREAL_1:7;
then cost(Q,W) <= cost(s,W) by A56,XXREAL_0:2;
hence cost(Q,W) <= cost(S,W) by A11,XXREAL_0:2;
end;
end;
Q is_orientedpath_of v1,v3,V by A5,GRAPH_5:def 18;
then Q is_orientedpath_of v1,v3,V9 by GRAPH_5:32,XBOOLE_1:7;
hence thesis by A8,GRAPH_5:def 18;
end;
reserve G for finite oriented Graph,
P,Q for oriented Chain of G,
W for Function of (the carrier' of G), Real>=0,
v1,v2,v3,v4 for Vertex of G;
theorem Th14:
e in the carrier' of G & P=<*e*> & e orientedly_joins v1,v2
implies P is_shortestpath_of v1,v2,{v1},W
proof
assume that
A1: e in the carrier' of G and
A2: P=<*e*> and
A3: e orientedly_joins v1,v2;
A4: len P = 1 by A2,FINSEQ_1:40;
then
A5: vertices(P)=vertices(P/.1) by GRAPH_5:25;
set FS=the Source of G, FT=the Target of G, Eg=the carrier' of G;
A6: FS.e = v1 & FT.e = v2 by A3,GRAPH_4:def 1;
A7: now
let S be oriented Chain of G;
assume
A8: S is_orientedpath_of v1,v2,{v1};
W is_weight>=0of G by GRAPH_5:def 13;
then consider s being Simple oriented Chain of G such that
A9: s is_shortestpath_of v1,v2,{v1},W by A8,GRAPH_5:62;
set Vs=vertices s;
A10: s is_orientedpath_of v1,v2,{v1} by A9,GRAPH_5:def 18;
then
A11: s is_orientedpath_of v1,v2 by GRAPH_5:def 4;
then s <> {} by GRAPH_5:def 3;
then
len s >=1 by FINSEQ_1:20;
then consider i being Nat such that
A12: len s = 1+i by NAT_1:10;
A13: FT.(s.len s)=v2 by A11,GRAPH_5:def 3;
A14: FS.(s.1)=v1 by A11,GRAPH_5:def 3;
consider s1,s2 being FinSequence such that
A15: len s1 = i and
A16: len s2 = 1 and
A17: s = s1^s2 by A12,FINSEQ_2:22;
reconsider s1,s2 as Simple oriented Chain of G by A17,GRAPH_5:14;
Vs \ {v2} c= {v1} by A10,GRAPH_5:def 4;
then Vs c= {v2} \/ {v1} by XBOOLE_1:44;
then
A18: Vs c= {v1,v2} by ENUMSET1:1;
now
reconsider vx=FS.(s2.1) as Vertex of G by A16,Lm3;
A19: len s1 < len s by A12,A15,NAT_1:13;
A20: vx in vertices(s2) by A16,Lm4;
vertices(s2) c= vertices(s1^s2) by GRAPH_5:26;
then
A21: vertices(s2) c= {v1,v2} by A18,A17;
assume s1 <> {};
then
A22: len s1 >=1 by FINSEQ_1:20;
then
A23: FS.(s.1) <> FS.(s2.1) by A16,A17,Th6;
len s2 =1 by A16;
then
A24: FT.(s.len s) <> FT.(s1.len s1) by A17,A22,Th6;
FS.(s2.1)=FS.(s.(len s1+1)) by A16,A17,Lm2
.=FT.(s.len s1) by A22,A19,GRAPH_1:def 15
.=FT.(s1.len s1) by A17,A22,Lm1;
hence contradiction by A14,A13,A24,A23,A21,A20,TARSKI:def 2;
end;
then
A25: len s= 0+1 by A12,A15;
s/.1 in Eg by A1;
then s.1 in Eg by A25,FINSEQ_4:15;
then e = s.1 by A1,A6,A14,A13,A25,GRAPH_1:def 7;
then s = P by A2,A25,FINSEQ_1:40;
hence cost(P,W) <= cost(S,W) by A8,A9,GRAPH_5:def 18;
end;
A26: P.1=e by A2;
then P/.1=e by A4,FINSEQ_4:15;
then vertices(P)={v1,v2} by A6,A5,GRAPH_5:def 1;
then
A27: vertices(P) \ {v2} = ({v1} \/ {v2}) \{v2} by ENUMSET1:1
.={v1} \ {v2} by XBOOLE_1:40;
P is_orientedpath_of v1,v2 by A2,A6,A4,A26,GRAPH_5:def 3;
then P is_orientedpath_of v1,v2,{v1} by A27,GRAPH_5:def 4;
hence thesis by A7,GRAPH_5:def 18;
end;
theorem Th15:
e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <>
v3 & Q=P^<*e*> & e orientedly_joins v2,v3 & v1 in V & (for v4 st v4 in V holds
not (ex ee st ee in the carrier' of G & ee orientedly_joins v4,v3)) implies Q
is_shortestpath_of v1,v3,V \/{v2},W
proof
assume that
A1: e in the carrier' of G and
A2: P is_shortestpath_of v1,v2,V,W and
A3: v1 <> v3 and
A4: Q=P^<*e*> and
A5: e orientedly_joins v2,v3 and
A6: v1 in V and
A7: for v4 st v4 in V holds not (ex ee st ee in the carrier' of G & ee
orientedly_joins v4,v3);
set Eg=the carrier' of G;
reconsider pe=<*e*> as FinSequence of Eg by A1,FINSEQ_1:74;
A8: P is_orientedpath_of v1,v2,V by A2,GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
then P <> {} by GRAPH_5:def 3;
then
A9: len P >=1 by FINSEQ_1:20;
set V9=V \/ {v2}, FS=the Source of G, FT=the Target of G;
A10: W is_weight>=0of G by GRAPH_5:def 13;
A11: now
let S be oriented Chain of G;
assume
A12: S is_orientedpath_of v1,v3,V9;
then consider s being Simple oriented Chain of G such that
A13: s is_shortestpath_of v1,v3,V9,W by A10,GRAPH_5:62;
set Vs=vertices s;
A14: s is_orientedpath_of v1,v3,V9 by A13,GRAPH_5:def 18;
then
A15: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;
then
A16: FT.(s.len s)=v3 by GRAPH_5:def 3;
A17: Vs \ {v3} c= V9 by A14,GRAPH_5:def 4;
s <> {} by A15,GRAPH_5:def 3;
then
A18: len s >=1 by FINSEQ_1:20;
then consider i being Nat such that
A19: len s = 1+i by NAT_1:10;
consider s1,s2 being FinSequence such that
A20: len s1 = i and
A21: len s2 = 1 and
A22: s = s1^s2 by A19,FINSEQ_2:22;
reconsider s1,s2 as Simple oriented Chain of G by A22,GRAPH_5:14;
reconsider vx=FS.(s2.1) as Vertex of G by A21,Lm3;
A23: s2.1= s.len s by A19,A20,A21,A22,Lm2;
A24: FS.(s.1)=v1 by A15,GRAPH_5:def 3;
A25: s1 <> {}
proof
assume s1 = {};
then
A26: len s= 1+ 0 by A19,A20;
then s.1 orientedly_joins v1,v3 by A24,A16,GRAPH_4:def 1;
hence contradiction by A6,A7,A26,Th2;
end;
then
A27: len s1 >=1 by FINSEQ_1:20;
len s1 < len s by A19,A20,NAT_1:13;
then
A28: FS.(s.len s)=FT.(s.len s1) by A19,A20,A27,GRAPH_1:def 15
.=FT.(s1.len s1) by A22,A27,Lm1;
A29: now
vx <> FT.(s.len s) by A21,A22,A23,A27,A28,Th6;
then
A30: not vx in {v3} by A16,TARSKI:def 1;
vx in Vs by A18,A23,Lm4;
then vx in (Vs \ {v3}) by A30,XBOOLE_0:def 5;
then
A31: vx in V or vx in {v2} by A17,XBOOLE_0:def 3;
assume
A32: vx <> v2;
s2.1 orientedly_joins vx,v3 & s2.1 in the carrier' of G by A21,A23,A16
,Th2,GRAPH_4:def 1;
hence contradiction by A7,A32,A31,TARSKI:def 1;
end;
len s2 = 1 by A21;
then not FT.(s.len s) in vertices(s1) by A3,A22,A24,A16,A27,GRAPH_5:18;
then
A33: vertices(s1) \ {v3} = vertices(s1) by A16,ZFMISC_1:57;
vertices(s1) c= vertices(s1^s2) by GRAPH_5:26;
then vertices(s1) c= Vs \ {v3} by A22,A33,XBOOLE_1:33;
then vertices(s1) c= V9 by A17;
then vertices(s1) \ {v2} c= V9 \ {v2} by XBOOLE_1:33;
then vertices(s1) \ {v2} c= V \ {v2} by XBOOLE_1:40;
then
A34: vertices(s1) \ {v2} c= V by XBOOLE_1:1;
s2/.1 in Eg by A1;
then
A35: s2.1 in Eg by A21,FINSEQ_4:15;
FS.e = v2 & FT.e = v3 by A5,GRAPH_4:def 1;
then e = s2.1 by A1,A23,A16,A29,A35,GRAPH_1:def 7;
then s2 = <*e*> by A21,FINSEQ_1:40;
then
A36: cost(Q,W)=cost(P,W)+cost(s2,W) by A4,A10,GRAPH_5:46,54;
FS.(s1.1)=v1 by A22,A24,A27,Lm1;
then s1 is_orientedpath_of v1,v2 by A23,A25,A28,A29,GRAPH_5:def 3;
then s1 is_orientedpath_of v1,v2,V by A34,GRAPH_5:def 4;
then
A37: cost(P,W) <= cost(s1,W) by A2,GRAPH_5:def 18;
A38: cost(s,W) <= cost(S,W) by A12,A13,GRAPH_5:def 18;
cost(s,W)=cost(s1,W)+cost(s2,W) by A10,A22,GRAPH_5:46,54;
then cost(Q,W) <= cost(s,W) by A37,A36,XREAL_1:7;
hence cost(Q,W) <= cost(S,W) by A38,XXREAL_0:2;
end;
len pe = 1 & pe.1=e by FINSEQ_1:40;
then Q is_orientedpath_of v1,v3,V9 by A4,A5,A8,A9,GRAPH_5:34;
hence thesis by A11,GRAPH_5:def 18;
end;
theorem Th16:
the carrier of G= U \/ V & v1 in U & (for v3,v4 st v3 in U & v4
in V holds not (ex e st e in the carrier' of G & e orientedly_joins v3,v4))
implies (P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W)
proof
assume
A1: the carrier of G= U \/ V & v1 in U & for v3,v4 st v3 in U & v4 in V
holds not (ex e st e in the carrier' of G & e orientedly_joins v3,v4);
hereby
assume
A2: P is_shortestpath_of v1,v2,U,W;
A3: now
let Q;
assume Q is_orientedpath_of v1,v2;
then Q is_orientedpath_of v1,v2,U by A1,Th12;
hence cost(P,W) <= cost(Q,W) by A2,GRAPH_5:def 18;
end;
P is_orientedpath_of v1,v2,U by A2,GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
hence P is_shortestpath_of v1,v2,W by A3,GRAPH_5:def 17;
end;
hereby
assume
A4: P is_shortestpath_of v1,v2,W;
A5: now
let Q;
assume Q is_orientedpath_of v1,v2,U;
then Q is_orientedpath_of v1,v2 by GRAPH_5:def 4;
hence cost(P,W) <= cost(Q,W) by A4,GRAPH_5:def 17;
end;
P is_orientedpath_of v1,v2 by A4,GRAPH_5:def 17;
then P is_orientedpath_of v1,v2,U by A1,Th12;
hence P is_shortestpath_of v1,v2,U,W by A5,GRAPH_5:def 18;
end;
end;
begin :: The definition of assignment statement
notation
let f be Function, i, x be object;
synonym (f,i):=x for f+*(i,x);
end;
definition
let f be FinSequence of REAL, x be object, r be Real;
redefine func (f, x):=r -> FinSequence of REAL; :: redefines := (GRAPHSP, synonym) → +* (FUNCT_7, definition)
coherence
proof
A1: rng ((f, x):=r) c= REAL
proof
let y be object;
A2: rng ((f, x):=r) c= rng f \/ {r} by FUNCT_7:100;
A3: r in REAL by XREAL_0:def 1;
assume y in rng ((f, x):=r);
then y in rng f or y in {r} by A2,XBOOLE_0:def 3;
hence thesis by A3,TARSKI:def 1;
end;
dom ((f, x):=r) = dom f by FUNCT_7:30
.= Seg (len f) by FINSEQ_1:def 3;
then (f, x):=r is FinSequence by FINSEQ_1:def 2;
hence thesis by A1,FINSEQ_1:def 4;
end;
end;
definition
let i,k be Nat,f be FinSequence of REAL,r be Real;
func (f,i):=(k,r) -> FinSequence of REAL equals
((f,i):=k,k):=r;
coherence;
end;
reserve f,g,h for Element of REAL*,
r for Real;
theorem Th17:
i <> k & i in dom f implies ((f,i):=(k,r)).i = k
proof
assume that
A1: i <> k and
A2: i in dom f;
set fik = (f,i):=k;
thus ((f,i):=(k,r)).i =fik.i by A1,FUNCT_7:32
.=k by A2,FUNCT_7:31;
end;
theorem Th18:
m <> i & m <> k implies ((f,i):=(k,r)).m = f.m
proof
assume that
A1: m <> i and
A2: m <> k;
set fik = (f,i):=k;
thus ((f,i):=(k,r)).m =fik.m by A2,FUNCT_7:32
.=f.m by A1,FUNCT_7:32;
end;
theorem Th19:
k in dom f implies ((f,i):=(k,r)).k = r
proof
set fik = (f,i):=k;
A1: dom fik = dom f by FUNCT_7:30;
assume k in dom f;
hence thesis by A1,FUNCT_7:31;
end;
theorem Th20:
dom ((f,i):=(k,r)) = dom f
proof
set fik = (f,i):=k;
thus dom ((f,i):=(k,r)) =dom fik by FUNCT_7:30
.=dom f by FUNCT_7:30;
end;
begin :: The definition of Pascal-like while-do statement
definition
let X be set,f,g be Element of Funcs(X,X);
redefine func g*f -> Element of Funcs(X,X); :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
reconsider f,g as Function of X,X by FUNCT_2:66;
g*f in Funcs(X,X) by FUNCT_2:9;
hence thesis;
end;
end;
definition
let X be set,f be Element of Funcs(X,X),g be Element of X;
redefine func f.g -> Element of X; :: redefines . (FUNCT_1, definition)
coherence
proof
A1: f is Function of X,X by FUNCT_2:66;
per cases;
suppose
A2: X = {};
then {} = dom f by A1;
then f.g = {} by FUNCT_1:def 2;
hence thesis by A2,SUBSET_1:def 1;
end;
suppose
X <> {};
hence thesis by A1,FUNCT_2:5;
end;
end;
end;
definition
let X be set, f be Element of Funcs(X,X);
func repeat(f) -> sequence of Funcs(X,X) means
:Def2:
it.0 = id X & for i being Nat holds it.(i+1)=f*(it.i);
existence
proof
deffunc G(Nat,Element of Funcs(X,X)) = f*$2;
ex F being sequence of Funcs(X,X) st F.0 = id X & for n being Nat
holds F.(n+1) = G(n,F.n) from NAT_1:sch 12;
hence thesis;
end;
uniqueness
proof
deffunc R(Nat,Element of Funcs(X,X)) = f*$2;
let F1,F2 be sequence of Funcs(X,X) such that
A1: F1.0 = id X and
A2: for i being Nat holds F1.(i+1)=R(i,F1.i) and
A3: F2.0 = id X and
A4: for i being Nat holds F2.(i+1)=R(i,F2.i);
thus F1 = F2 from NAT_1:sch 16(A1,A2,A3,A4);
end;
end;
theorem Th21:
for F being Element of Funcs(REAL*,REAL*), f being Element of
REAL*,n,i be Element of NAT holds (repeat F).0 .f = f
proof
let F be Element of Funcs(REAL*,REAL*), f be Element of REAL*,n,i be Element
of NAT;
thus (repeat F).0 .f = (id (REAL*)).f by Def2
.= f;
end;
Lm5: for X being set,f being Element of Funcs(X,X) holds dom f=X
proof
let X be set, f be Element of Funcs(X,X);
ex ff being Function st f = ff & dom ff = X & rng ff c= X by FUNCT_2:def 2;
hence thesis;
end;
theorem Th22:
for F,G being Element of Funcs(REAL*,REAL*),f being Element of
REAL*, i be Nat holds (repeat (F*G)).(i+1).f = F.(G.((repeat (F*G)).
i.f))
proof
let F,G be Element of Funcs(REAL*,REAL*),f be Element of REAL*,i;
set Fi=(repeat (F*G)).i, ff=Fi.f, FFi=(F*G)*Fi;
A1: dom (F*G) = REAL* by Lm5;
A2: dom FFi=REAL* by Lm5;
thus (repeat (F*G)).(i+1).f=FFi.f by Def2
.=(F*G).ff by A2,FUNCT_1:12
.=F.(G.ff) by A1,FUNCT_1:12;
end;
definition
let g be Element of Funcs(REAL*,REAL*),f be Element of REAL*;
redefine func g.f -> Element of REAL*; :: redefines . (FUNCT_1, definition)
coherence
proof
g.f in REAL*;
hence thesis;
end;
end;
definition
let f be Element of REAL*, n be Nat;
func OuterVx(f,n) -> Subset of NAT equals
{i: i in dom f & 1 <= i & i <= n &
f.i <> -1 & f.(n+i) <> -1};
coherence
proof
set NS={i: i in dom f & 1 <= i & i <= n & f.i <> -1 & f.(n+i) <> -1};
NS c= NAT
proof
let x be object;
assume x in NS;
then
ex k being Nat st x=k & k in dom f & 1 <= k & k <= n & f.k
<> -1 & f.(n+k) <> -1;
hence thesis;
end;
hence thesis;
end;
end;
definition
let f be Element of Funcs(REAL*,REAL*),g be Element of REAL*, n be Nat;
assume
A1: ex i st OuterVx((repeat f).i.g,n) = {};
func LifeSpan(f,g,n) -> Element of NAT means
:Def4:
OuterVx((repeat f).it.g,
n) = {} & for k being Nat st OuterVx((repeat f).k.g,n) = {} holds it <= k;
existence
proof
defpred P[Nat] means OuterVx((repeat f).$1.g,n) = {};
A2: ex k be Nat st P[k] by A1;
ex k be Nat st P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch
5(A2);
then consider k be Nat such that
A3: ( P[k])& for n be Nat st P[n] holds k <= n;
k in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
uniqueness
proof
let it1, it2 be Element of NAT;
assume
A4: not thesis;
then it1 <= it2 & it2 <= it1;
hence contradiction by A4,XXREAL_0:1;
end;
end;
definition
let f be Element of Funcs(REAL*,REAL*), n be Nat;
func while_do(f,n) -> Element of Funcs(REAL*,REAL*) means
:Def5:
dom it=REAL
* & for h being Element of REAL* holds it.h=(repeat f).LifeSpan(f,h,n).h;
existence
proof
set X=REAL*;
defpred P[object,object] means
for h being Element of X st $1=h holds $2=(repeat
f).LifeSpan(f,h,n).h;
A1: ex ff being Function st f = ff & dom ff = X & rng ff c= X by FUNCT_2:def 2;
A2: now
let xx be object;
assume xx in dom f;
then reconsider h9=xx as Element of X by A1;
now
take yy=(repeat f).LifeSpan(f,h9,n).h9;
let h be Element of X;
assume xx=h;
hence yy=(repeat f).LifeSpan(f,h,n).h;
end;
hence ex y1 being object st P[xx,y1];
end;
consider f9 being Function such that
A3: dom f9=dom f & for xx being object st xx in dom f holds P[xx, f9.xx]
from CLASSES1:sch 1(A2);
rng f9 c= X
proof
let y be object;
assume y in rng f9;
then consider xx being object such that
A4: xx in dom f9 and
A5: y = f9.xx by FUNCT_1:def 3;
reconsider h9=xx as Element of X by A1,A3,A4;
y=(repeat f).LifeSpan(f,h9,n).h9 by A3,A4,A5;
hence thesis;
end;
then reconsider f9 as Element of Funcs(X,X) by A1,A3,FUNCT_2:def 2;
take f9;
thus dom f9 = X by A1,A3;
let h be Element of X;
thus thesis by A1,A3;
end;
uniqueness
proof
set X=REAL*;
let g1,g2 be Element of Funcs(X,X) such that
A6: dom g1 = X and
A7: for h being Element of X holds g1.h=(repeat f).LifeSpan(f,h,n).h and
A8: dom g2 = X and
A9: for h being Element of X holds g2.h=(repeat f).LifeSpan(f,h,n).h;
now
let xx be object;
assume xx in dom g1;
then reconsider h=xx as Element of X by A6;
thus g1.xx=(repeat f).LifeSpan(f,h,n).h by A7
.=g2.xx by A9;
end;
hence thesis by A6,A8,FUNCT_1:2;
end;
end;
begin :: Defining a weight function for an oriented graph
definition
let G be oriented Graph,v1,v2 be Vertex of G;
assume
A1: ex e be set st e in the carrier' of G & e orientedly_joins v1,v2;
func XEdge(v1,v2) -> set means
:Def6:
ex e be set st it = e & e in the carrier' of G & e orientedly_joins v1,v2;
existence by A1;
uniqueness by Th10;
end;
definition
let G be oriented Graph,v1,v2 be Vertex of G, W be Function;
func Weight(v1,v2,W) -> set equals
:Def7:
W.XEdge(v1,v2) if ex e be set st e in the
carrier' of G & e orientedly_joins v1,v2 otherwise -1;
correctness by TARSKI:1;
end;
registration
let G be oriented Graph,v1,v2 be Vertex of G, W be Function of (the carrier'
of G), Real>=0;
cluster Weight(v1,v2,W) -> real;
coherence
proof
per cases;
suppose
A1: ex e be set st e in the carrier' of G & e orientedly_joins v1,v2;
then consider e being set such that
A2: XEdge(v1,v2) = e and
A3: e in the carrier' of G and
e orientedly_joins v1,v2 by Def6;
e in dom W by A3,FUNCT_2:def 1;
then W.XEdge(v1,v2) in Real>=0 by A2,PARTFUN1:4;
hence thesis by A1,Def7;
end;
suppose
not ex e be set st e in the carrier' of G & e orientedly_joins v1,v2;
hence thesis by Def7;
end;
end;
end;
reserve G for oriented Graph,
v1,v2 for Vertex of G,
W for Function of (the carrier' of G), Real>=0;
theorem Th23:
Weight(v1,v2,W) >= 0 iff ex e be set st e in the carrier' of G &
e orientedly_joins v1,v2
proof
set EG=the carrier' of G;
thus Weight(v1,v2,W) >= 0 implies
ex e be set st e in EG & e orientedly_joins v1,v2 by Def7;
assume ex e be set st e in the carrier' of G & e orientedly_joins v1,v2;
then consider e being set such that
A1: XEdge(v1,v2) = e and
A2: e in EG and
A3: e orientedly_joins v1,v2 by Def6;
e in dom W by A2,FUNCT_2:def 1;
then W.e in Real>=0 by PARTFUN1:4;
then ex r being Real st W.e=r & r >=0 by GRAPH_5:def 12;
hence thesis by A1,A2,A3,Def7;
end;
theorem
Weight(v1,v2,W) = -1 iff not ex e be set st e in the carrier' of G & e
orientedly_joins v1,v2 by Def7,Th23;
theorem Th25:
e in the carrier' of G & e orientedly_joins v1,v2 implies Weight
(v1,v2,W)=W.e
proof
set EG=the carrier' of G;
assume
A1: e in EG & e orientedly_joins v1,v2;
then consider e1 being set such that
A2: XEdge(v1,v2) = e1 and
A3: e1 in EG & e1 orientedly_joins v1,v2 by Def6;
e=e1 by A1,A3,Th10;
hence thesis by A2,A3,Def7;
end;
begin :: Basic operations for Dijkstra's shortest path algorithm
definition
let f be Element of REAL*, n be Nat;
func UnusedVx(f,n) -> Subset of NAT equals
{i: i in dom f & 1 <= i & i <= n
& f.i <> -1};
coherence
proof
set NS={i: i in dom f & 1 <= i & i <= n & f.i <> -1};
NS c= NAT
proof
let x be object;
assume x in NS;
then
ex k being Nat st x=k & k in dom f & 1 <= k & k <= n & f.k
<> -1;
hence thesis;
end;
hence thesis;
end;
end;
definition
let f be Element of REAL*, n be Nat;
func UsedVx(f,n) -> Subset of NAT equals
{i: i in dom f & 1 <= i & i <= n &
f.i = -1};
coherence
proof
set NS={i: i in dom f & 1 <= i & i <= n & f.i = -1};
NS c= NAT
proof
let x be object;
assume x in NS;
then
ex k being Nat st x=k & k in dom f & 1 <= k & k <= n & f.k
= -1;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th26:
UnusedVx(f,n) c= Seg n
proof
let x be object;
assume x in UnusedVx(f,n);
then ex i st x=i & i in dom f & 1 <= i & i <= n & f.i <> - 1;
then x in {k where k is Nat: 1 <= k & k <= n };
hence thesis by FINSEQ_1:def 1;
end;
registration
let f be Element of REAL*, n be Nat;
cluster UnusedVx(f,n) -> finite;
coherence
proof
UnusedVx(f,n) c= Seg n by Th26;
hence thesis;
end;
end;
theorem Th27:
OuterVx(f,n) c= UnusedVx(f,n)
proof
let x be object;
assume x in OuterVx(f,n);
then ex k st x=k & k in dom f & 1 <= k & k <= n & f.k <> - 1 & f.(n+k) <> -1;
hence thesis;
end;
theorem Th28:
OuterVx(f,n) c= Seg n
proof
OuterVx(f,n) c= UnusedVx(f,n) & UnusedVx(f,n) c= Seg n by Th26,Th27;
hence thesis;
end;
registration
let f be Element of REAL*, n be Nat;
cluster OuterVx(f,n) -> finite;
coherence
proof
OuterVx(f,n) c= Seg n by Th28;
hence thesis;
end;
end;
definition
let X be finite Subset of NAT,f be Element of REAL*,n;
func Argmin(X,f,n) -> Nat means
:Def10:
(X<>{} implies ex i st i=
it & i in X & (for k st k in X holds f/.(2*n+i) <= f/.(2*n+k)) & for k st k in
X & f/.(2*n+i) = f/.(2*n+k) holds i <= k ) & (X={} implies it=0);
existence
proof
per cases;
suppose
A1: X={};
take 0;
thus thesis by A1;
end;
suppose
A2: X<>{};
then reconsider X9=X as non empty finite Subset of NAT;
deffunc F(Element of X9)= f/.(2*n+$1);
consider x being Element of X9 such that
A3: for y being Element of X9 holds F(x) <= F(y) from PRE_CIRC:sch 5;
reconsider x as Element of NAT;
defpred P[Nat] means $1 in X & f/.(2*n+x) = f/.(2*n+$1);
A4: ex i be Nat st P[i];
consider i be Nat such that
A5: P[i] & for k be Nat st P[k] holds i <= k from NAT_1:sch 5(A4);
::: reconsider i as Element of NAT by ORDINAL1:def 12;
take F=i;
hereby
assume X<>{};
take i=F;
thus i=F & i in X by A5;
thus for k st k in X holds f/.(2*n+i) <= f/.(2*n+k) by A3,A5;
thus for k st k in X & f/.(2*n+i) = f/.(2*n+k) holds i <= k by A5;
end;
thus thesis by A2;
end;
end;
uniqueness
proof
let F1,F2 be Nat such that
A6: X<>{} implies ex i st i=F1 & i in X & (for k st k in X holds f/.(2
*n+i ) <= f/.(2*n+k)) & for k st k in X & f/.(2*n+i) = f/.(2*n+k) holds i <= k
and
A7: X={} implies F1=0 and
A8: X<>{} implies ex i st i=F2 & i in X & (for k st k in X holds f/.(2
*n+i) <= f/.(2*n+k)) & for k st k in X & f/.(2*n+i) = f/.(2*n+k) holds i <= k
and
A9: X={} implies F2=0;
per cases;
suppose
A10: X<>{};
then consider j such that
A11: j=F2 and
A12: j in X and
A13: for k st k in X holds f/.(2*n+j) <= f/.(2*n+k) and
A14: for k st k in X & f/.(2*n+j) = f/.(2*n+k) holds j <= k by A8;
consider i such that
A15: i=F1 and
A16: i in X and
A17: for k st k in X holds f/.(2*n+i) <= f/.(2*n+k) and
A18: for k st k in X & f/.(2*n+i) = f/.(2*n+k) holds i <= k by A6,A10;
f/.(2*n+i) <= f/.(2*n+j) & f/.(2*n+j) <= f/.(2*n+i) by A16,A17,A12,A13;
then f/.(2*n+j) = f/.(2*n+i) by XXREAL_0:1;
then i <= j & j <= i by A16,A18,A12,A14;
hence thesis by A15,A11,XXREAL_0:1;
end;
suppose
X={};
hence thesis by A7,A9;
end;
end;
end;
theorem Th29:
OuterVx(f,n) <> {} & j=Argmin(OuterVx(f,n),f,n) implies j in dom
f & 1<=j & j<=n & f.j <> -1 & f.(n+j) <> -1
proof
set IN=OuterVx(f,n);
assume IN <> {} & j=Argmin(IN,f,n);
then
ex i st i=j & i in IN &( for k st k in IN holds f/.(2*n+ i) <= f/.(2*n+k)
)& for k st k in IN & f/.(2*n+i) = f/.(2*n+k) holds i <= k by Def10;
then
ex k st j=k & k in dom f & 1 <= k & k<= n & f.k <> -1 & f.(n+k) <> -1;
hence thesis;
end;
theorem Th30:
Argmin(OuterVx(f,n),f,n) <= n
proof
set IN=OuterVx(f,n);
per cases;
suppose
IN <> {};
hence thesis by Th29;
end;
suppose
IN = {};
hence thesis by Def10;
end;
end;
definition
let n be Nat;
func findmin(n) -> Element of Funcs(REAL*,REAL*) means
:Def11:
dom it = REAL* &
for f be Element of REAL*
holds it.f= (f,n*n+3*n+1) := (Argmin(OuterVx(f,n),f,n),-1);
existence
proof
set X=REAL*, mi=n*n+3*n+1;
defpred P[object,object] means
for f be Element of REAL* st $1=f holds $2= (f,mi
):=(Argmin(OuterVx(f,n),f,n),-1);
A1: now
let xx be object;
assume xx in X;
then reconsider h=xx as Element of REAL*;
reconsider y= (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) as object;
take y;
thus P[xx,y];
end;
consider F being Function such that
A2: dom F=X &
for x being object st x in X holds P[x,F.x] from CLASSES1:sch 1(A1);
rng F c= X
proof
let y be object;
assume y in rng F;
then consider xx being object such that
A3: xx in dom F and
A4: y = F.xx by FUNCT_1:def 3;
reconsider h=xx as Element of REAL* by A2,A3;
y = (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) by A2,A4;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider F as Element of Funcs(X,X) by A2,FUNCT_2:def 2;
take F;
thus dom F = X by A2;
let f be Element of REAL*;
thus thesis by A2;
end;
uniqueness
proof
set X=REAL*, mi=n*n+3*n+1;
let F1,F2 be Element of Funcs(X,X) such that
A5: dom F1= X and
A6: for f be Element of REAL* holds F1.f= (f,mi):=(Argmin(OuterVx(f,n
), f,n),-1) and
A7: dom F2= X and
A8: for f be Element of REAL* holds F2.f= (f,mi):=(Argmin(OuterVx(f,n
), f,n),-1);
now
let xx be object;
assume xx in dom F1;
then reconsider h=xx as Element of REAL* by A5;
thus F1.xx= (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) by A6
.=F2.xx by A8;
end;
hence thesis by A5,A7,FUNCT_1:2;
end;
end;
reconsider jj=1 as Real;
theorem Th31:
i > n & i <> n*n+3*n+1 implies (findmin n).f.i=f.i
proof
set k=Argmin(OuterVx(f,n),f,n), mi=n*n+3*n+1;
assume
A1: i > n & i <> mi;
(findmin n).f.i = ((f,mi):=(k,-jj)).i & k <= n by Def11,Th30;
hence thesis by A1,Th18;
end;
theorem Th32:
i in dom f & f.i=-1 & i <> n*n+3*n+1 implies (findmin n).f.i=-1
proof
set k=Argmin(OuterVx(f,n),f,n), mi=n*n+3*n+1;
assume that
A1: i in dom f and
A2: f.i=-1 & i <> mi;
A3: (findmin n).f.i = ((f,mi):=(k,-jj)).i by Def11;
per cases;
suppose
i=k;
hence thesis by A1,A3,Th19;
end;
suppose
i<>k;
hence thesis by A2,A3,Th18;
end;
end;
theorem Th33:
dom ((findmin n).f) = dom f
proof
(findmin n).f = (f,n*n+3*n+1):=(Argmin(OuterVx(f,n),f,n),-jj) by Def11;
hence thesis by Th20;
end;
Lm6: k>=1 implies n <= k*n
proof
assume k >= 1;
then 1*n <= k*n by NAT_1:4;
hence thesis;
end;
Lm7: 3*n < n*n+3*n+1 & n < n*n+3*n+1 & 2*n < n*n+3*n+1
proof
3*n <= n*n+3*n by NAT_1:12;
hence
A1: 3*n < n*n+3*n +1 by NAT_1:13;
n <= 3*n by Lm6;
hence n < n*n+3*n+1 by A1,XXREAL_0:2;
2*n <= 3*n by NAT_1:4;
hence thesis by A1,XXREAL_0:2;
end;
Lm8: (n<k & k <= 2*n implies not (2*n<k & k <= 3*n) & not (k <=n or k > 3*n))
& ((k <=n or k > 3*n) implies not (2*n<k & k <= 3*n) & not (n<k & k <= 2*n))& (
2*n<k & k <= 3*n implies not (n<k & k <= 2*n) & not (k <=n or k > 3*n))
proof
A1: 2*n <= 3*n by NAT_1:4;
hence
n<k & k <= 2*n implies (not (2*n<k & k <= 3*n)) & not (k <= n or k > 3*
n) by XXREAL_0:2;
A2: 2*n = n+n;
hereby
assume
A3: k <= n or k > 3*n;
per cases by A3;
suppose
A4: k <= n;
hence not (2*n<k & k <= 3*n) by A2,NAT_1:12;
thus not (n<k & k <= 2*n) by A4;
end;
suppose
A5: k > 3*n;
hence not (2*n<k & k <= 3*n);
thus not (n<k & k <= 2*n) by A1,A5,XXREAL_0:2;
end;
end;
assume that
A6: 2*n<k and
A7: k <= 3*n;
thus not (n<k & k <= 2*n) by A6;
thus thesis by A2,A6,A7,NAT_1:12;
end;
theorem Th34:
OuterVx(f,n) <> {} implies ex j st j in OuterVx(f,n) & 1 <= j &
j <= n & (findmin n).f.j=-1
proof
set IX=OuterVx(f,n);
assume IX <> {};
then consider i such that
A1: i=Argmin(IX,f,n) and
A2: i in IX and
for k st k in IX holds f/.(2*n+i) <= f/.(2*n+k) and
for k st k in IX & f/.(2*n+i) = f/.(2*n+k) holds i <= k by Def10;
take i;
thus i in IX by A2;
A3: ex k st i=k & k in dom f & 1 <= k & k <= n & f.k <> - 1 & f.(n+k) <> -1
by A2;
hence 1 <= i & i <= n;
thus (findmin n).f.i = ((f,n*n+3*n+1):=(i,-jj)).i by A1,Def11
.=-1 by A3,Th19;
end;
definition
let f be Element of REAL*,n,k be Nat;
func newpathcost(f,n,k) -> Real equals
f/.(2*n+f/.(n*n+3*n+1))+ f/.(2*n+n*(f
/.(n*n+3*n+1))+k);
correctness;
end;
definition
let n,k be Nat,f be Element of REAL*;
pred f hasBetterPathAt n,k means
(f.(n+k)=-1 or f/.(2*n+k) >
newpathcost(f,n,k)) & f/.(2*n+n*(f/.(n*n+3*n+1))+k) >= 0 & f.k <> -1;
end;
definition
let f be Element of REAL*,n be Nat;
func Relax(f,n) -> Element of REAL* means
:Def14:
dom it = dom f &
for k be Nat st k in dom f holds (n<k & k <= 2*n implies (f hasBetterPathAt n
,(k-'n) implies it.k=f/.(n*n+3*n+1)) & (not f hasBetterPathAt n,(k-'n) implies
it.k=f.k)) & (2*n <k & k <=3*n implies (f hasBetterPathAt n,(k-'2*n) implies it
.k=newpathcost(f,n,k-'2*n)) & (not f hasBetterPathAt n,(k-'2*n) implies it.k=f.
k)) & (k<=n or k > 3*n implies it.k=f.k);
existence
proof
defpred P2[Nat] means f hasBetterPathAt n,($1-'2*n);
defpred P1[Nat] means f hasBetterPathAt n,($1-'n);
set X=dom f;
defpred P[object,object] means
for k st $1=k & k in X holds (n<k & k <= 2*n
implies (P1[k] implies $2=f/.(n*n+3*n+1)) & (not P1[k] implies $2=f.k)) & (2*n
<k & k <=3*n implies (P2[k] implies $2=newpathcost(f,n,k-'2*n))& (not P2[k]
implies $2=f.k)) & (k<=n or k > 3*n implies $2=f.k);
A1: now
let xx be object;
assume xx in X;
then reconsider k=xx as Element of NAT;
per cases;
suppose
A2: n<k & k <= 2*n;
thus ex y1 being object st P[xx,y1]
proof
per cases;
suppose
A3: P1[k];
take y1 = f/.(n*n+3*n+1);
thus thesis by A2,A3,Lm8;
end;
suppose
A4: not P1[k];
take y1 = f.k;
thus thesis by A2,A4;
end;
end;
end;
suppose
A5: 2*n<k & k <= 3*n;
thus ex y1 being object st P[xx,y1]
proof
per cases;
suppose
A6: P2[k];
take y1 = newpathcost(f,n,k-'2*n);
thus thesis by A5,A6,Lm8;
end;
suppose
A7: not P2[k];
take y1 = f.k;
thus thesis by A5,A7;
end;
end;
end;
suppose
A8: k <=n or k > 3*n;
thus ex y1 being object st P[xx,y1]
proof
take y1=f.k;
thus thesis by A8,Lm8;
end;
end;
end;
consider F being Function such that
A9: dom F=X &
for x being object st x in X holds P[x,F.x] from CLASSES1:sch 1(A1);
A10: rng F c= REAL
proof
let y1 be object;
assume y1 in rng F;
then consider xx being object such that
A11: xx in dom F and
A12: y1 = F.xx by FUNCT_1:def 3;
reconsider k=xx as Element of NAT by A9,A11;
per cases;
suppose
A13: n<k & k <= 2*n;
hereby
per cases;
suppose
P1[k];
then y1 = f/.(n*n+3*n+1) by A9,A11,A12,A13;
hence thesis;
end;
suppose
not P1[k];
then y1 = f.k by A9,A11,A12,A13
.=f/.k by A9,A11,PARTFUN1:def 6;
hence thesis;
end;
end;
end;
suppose
A14: 2*n<k & k <= 3*n;
hereby
per cases;
suppose
P2[k];
then y1 = newpathcost(f,n,k-'2*n) by A9,A11,A12,A14;
hence thesis;
end;
suppose
not P2[k];
then y1 = f.k by A9,A11,A12,A14
.=f/.k by A9,A11,PARTFUN1:def 6;
hence thesis;
end;
end;
end;
suppose
k <=n or k > 3*n;
then y1 = f.k by A9,A11,A12
.=f/.k by A9,A11,PARTFUN1:def 6;
hence thesis;
end;
end;
X=Seg len f by FINSEQ_1:def 3;
then F is FinSequence by A9,FINSEQ_1:def 2;
then F is FinSequence of REAL by A10,FINSEQ_1:def 4;
then reconsider F as Element of REAL* by FINSEQ_1:def 11;
take F;
thus dom F = X by A9;
let k;
assume k in X;
hence thesis by A9;
end;
uniqueness
proof
let F1,F2 be Element of REAL* such that
A15: dom F1 = dom f and
A16: for k be Nat st k in dom f holds (n<k & k <= 2*n
implies (f hasBetterPathAt n,(k-'n) implies F1.k=f/.(n*n+3*n+1)) & (not f
hasBetterPathAt n,(k-'n) implies F1.k=f.k)) & (2*n <k & k <=3*n implies (f
hasBetterPathAt n,(k-'2*n) implies F1.k=newpathcost(f,n,k-'2*n)) & (not f
hasBetterPathAt n,(k-'2*n) implies F1.k=f.k)) & (k<=n or k > 3*n implies F1.k=f
.k) and
A17: dom F2 = dom f and
A18: for k be Nat st k in dom f holds (n<k & k <= 2*n
implies (f hasBetterPathAt n,(k-'n) implies F2.k=f/.(n*n+3*n+1)) & (not f
hasBetterPathAt n,(k-'n) implies F2.k=f.k)) & (2*n <k & k <=3*n implies (f
hasBetterPathAt n,(k-'2*n) implies F2.k=newpathcost(f,n,k-'2*n)) & (not f
hasBetterPathAt n,(k-'2*n) implies F2.k=f.k)) & (k<=n or k > 3*n implies F2.k=f
.k);
now
let xx be object;
assume
A19: xx in dom F1;
then reconsider k=xx as Element of NAT;
defpred P2[] means f hasBetterPathAt n,(k-'2*n);
defpred P1[] means f hasBetterPathAt n,(k-'n);
per cases;
suppose
A20: n<k & k <= 2*n;
hereby
per cases;
suppose
A21: P1[];
hence F1.xx = f/.(n*n+3*n+1) by A15,A16,A19,A20
.=F2.xx by A15,A18,A19,A20,A21;
end;
suppose
A22: not P1[];
hence F1.xx = f.k by A15,A16,A19,A20
.=F2.xx by A15,A18,A19,A20,A22;
end;
end;
end;
suppose
A23: 2*n<k & k <= 3*n;
hereby
per cases;
suppose
A24: P2[];
hence F1.xx = newpathcost(f,n,k-'2*n) by A15,A16,A19,A23
.=F2.xx by A15,A18,A19,A23,A24;
end;
suppose
A25: not P2[];
hence F1.xx = f.k by A15,A16,A19,A23
.=F2.xx by A15,A18,A19,A23,A25;
end;
end;
end;
suppose
A26: k <=n or k > 3*n;
hence F1.xx=f.k by A15,A16,A19
.=F2.xx by A15,A18,A19,A26;
end;
end;
hence thesis by A15,A17,FUNCT_1:2;
end;
end;
definition
let n be Nat;
func Relax(n) -> Element of Funcs(REAL*,REAL*) means
:Def15:
dom it = REAL* & for f be Element of REAL* holds it.f=Relax(f,n);
existence
proof
defpred P[object,object] means
for f be Element of REAL* st $1=f holds $2=Relax(
f,n);
set X=REAL*;
A1: now
let xx be object;
assume xx in X;
then reconsider h=xx as Element of REAL*;
thus ex y1 being object st P[xx,y1]
proof
take y1 = Relax(h,n);
thus thesis;
end;
end;
consider F being Function such that
A2: dom F=X &
for x being object st x in X holds P[x,F.x] from CLASSES1:sch 1(A1);
now
let y1 be object;
assume y1 in rng F;
then consider xx being object such that
A3: xx in dom F and
A4: y1 = F.xx by FUNCT_1:def 3;
reconsider h=xx as Element of REAL* by A2,A3;
y1 = Relax(h,n) by A2,A4;
hence y1 in X;
end;
then rng F c= X;
then reconsider F as Element of Funcs(X,X) by A2,FUNCT_2:def 2;
take F;
thus dom F = X by A2;
let f be Element of REAL*;
thus thesis by A2;
end;
uniqueness
proof
set X=REAL*;
let F1,F2 be Element of Funcs(X,X) such that
A5: dom F1= X and
A6: for f be Element of REAL* holds F1.f=Relax(f,n) and
A7: dom F2= X and
A8: for f be Element of REAL* holds F2.f=Relax(f,n);
now
let xx be object;
assume xx in dom F1;
then reconsider h=xx as Element of REAL* by A5;
thus F1.xx= Relax(h,n) by A6
.=F2.xx by A8;
end;
hence thesis by A5,A7,FUNCT_1:2;
end;
end;
theorem Th35:
dom ((Relax n).f) = dom f
proof
thus dom ((Relax n).f) = dom Relax(f,n) by Def15
.= dom f by Def14;
end;
theorem Th36:
(i <= n or i > 3*n) & i in dom f implies (Relax n).f.i=f.i
proof
assume
A1: ( i <= n or i > 3*n)& i in dom f;
thus (Relax n).f.i=Relax(f,n).i by Def15
.=f.i by A1,Def14;
end;
theorem Th37:
dom ((repeat(Relax(n)*findmin(n))).i.f) = dom ((repeat(Relax(n)*
findmin(n))).(i+1).f)
proof
set R=Relax(n), M=findmin(n), ff=(repeat (R*M)).i.f;
thus dom ((repeat (R*M)).(i+1).f) = dom (R.(M.ff)) by Th22
.= dom (M.ff) by Th35
.= dom ff by Th33;
end;
theorem Th38:
OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) <> {} implies
UnusedVx((repeat(Relax(n)*findmin(n))).(i+1).f,n) c< UnusedVx((repeat(Relax(n)*
findmin(n))).i.f,n)
proof
set R=Relax(n), M=findmin(n), ff=(repeat (R*M)).i.f;
set Fi1=(repeat (R*M)).(i+1).f;
assume OuterVx(ff,n) <> {};
then
A1: ex j st j in OuterVx(ff,n) & 1 <= j & j <= n & (M.ff). j=-1 by Th34;
A2: dom Fi1 = dom ff by Th37
.= dom (M.ff) by Th33;
A3: now
let x;
assume x in UnusedVx(Fi1,n);
then consider k such that
A4: x=k and
A5: k in dom Fi1 and
1 <= k and
A6: k <= n and
A7: Fi1.k <> -1;
Fi1.k=(R.(M.ff)).k by Th22
.=(M.ff).k by A2,A5,A6,Th36;
hence (M.ff).x <> -1 by A4,A7;
end;
A8: UnusedVx(Fi1,n) c= UnusedVx(ff,n)
proof
A9: n < n*n+3*n+1 by Lm7;
let x be object;
assume x in UnusedVx(Fi1,n);
then consider k such that
A10: x=k and
A11: k in dom Fi1 and
A12: 1 <= k and
A13: k <= n and
A14: Fi1.k <> -1;
A15: k in dom ff by A11,Th37;
Fi1.k=(R.(M.ff)).k by Th22
.=(M.ff).k by A2,A11,A13,Th36;
then ff.k <> -1 by A13,A14,A15,A9,Th32;
hence thesis by A10,A12,A13,A15;
end;
OuterVx(ff,n) c= UnusedVx(ff,n) by Th27;
then UnusedVx(Fi1,n) <> UnusedVx(ff,n) by A1,A3;
hence thesis by A8,XBOOLE_0:def 8;
end;
theorem Th39:
g=(repeat(Relax(n)*findmin(n))).i.f & h=(repeat(Relax(n)*findmin
(n))).(i+1).f & k=Argmin(OuterVx(g,n),g,n) & OuterVx(g,n) <> {} implies UsedVx(
h,n)=UsedVx(g,n) \/ {k} & not k in UsedVx(g,n)
proof
set R=Relax(n), M=findmin(n), ff=(repeat (R*M)).i.f, Fi1=(repeat (R*M)).(i+1
).f, mi=n*n+3*n+1;
assume that
A1: g=ff and
A2: h=Fi1 and
A3: k=Argmin(OuterVx(g,n),g,n) and
A4: OuterVx(g,n) <> {};
A5: M.ff = (ff,mi):=(k,-jj) by A1,A3,Def11;
A6: dom h = dom ff by A2,Th37;
A7: dom g=dom (M.ff) by A1,Th33;
A8: now
let x be object;
assume
A9: x in (UsedVx(g,n) \/ {k});
per cases by A9,XBOOLE_0:def 3;
suppose
A10: x in UsedVx(g,n);
A11: n < mi by Lm7;
consider m such that
A12: x=m and
A13: m in dom g and
A14: 1 <= m and
A15: m <= n and
A16: g.m = -1 by A10;
h.m=(R.(M.ff)).m by A2,Th22
.=(M.ff).m by A7,A13,A15,Th36
.=-1 by A1,A13,A15,A16,A11,Th32;
hence x in UsedVx(h,n) by A1,A6,A12,A13,A14,A15;
end;
suppose
x in {k};
then
A17: x = k by TARSKI:def 1;
A18: k in dom g by A3,A4,Th29;
A19: 1 <= k by A3,A4,Th29;
A20: k <= n by A3,A4,Th29;
h.k=(R.(M.ff)).k by A2,Th22
.=(M.ff).k by A7,A18,A20,Th36
.=-jj by A1,A5,A18,Th19;
hence x in UsedVx(h,n) by A1,A6,A17,A18,A19,A20;
end;
end;
A21: dom h = dom (M.ff) by A6,Th33;
now
let x be object;
assume x in UsedVx(h,n);
then consider m such that
A22: x=m and
A23: m in dom h and
A24: 1 <= m and
A25: m <= n and
A26: h.m = -1;
per cases;
suppose
m=k;
then x in {k} by A22,TARSKI:def 1;
hence x in (UsedVx(g,n) \/ {k}) by XBOOLE_0:def 3;
end;
suppose
A27: m<>k;
A28: n < mi by Lm7;
-1=(R.(M.ff)).m by A2,A26,Th22
.=(M.ff).m by A21,A23,A25,Th36
.=ff.m by A5,A25,A27,A28,Th18;
then
m in {j: j in dom ff & 1 <= j & j <= n & ff.j=-1} by A6,A23,A24,A25;
hence x in (UsedVx(g,n) \/ {k}) by A1,A22,XBOOLE_0:def 3;
end;
end;
hence UsedVx(h,n)=UsedVx(g,n) \/ {k} by A8,TARSKI:2;
assume k in UsedVx(g,n);
then ex j st j=k & j in dom g & 1 <= j & j <= n & g.j=-1;
hence contradiction by A3,A4,Th29;
end;
theorem Th40:
ex i st i<=n & OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) = {}
proof
set R=Relax n, M=findmin n;
defpred P[Nat] means
$1<=n implies card UnusedVx((repeat(R*M)).$1.f,n) <= n-$1;
set nf=(repeat(R*M)).n.f;
assume
A1: not ex i st i<=n & OuterVx((repeat(R*M)).i.f,n) = {};
A2: for k st P[k] holds P[k+1]
proof
let k;
assume
A3: P[k];
now
set fk=UnusedVx((repeat(R*M)).k.f,n), fk1=UnusedVx((repeat(R*M)).(k+1).f
,n);
A4: k <= k+1 by NAT_1:11;
assume
A5: k+1 <= n;
then OuterVx((repeat(R*M)).k.f,n) <> {} by A1,A4,XXREAL_0:2;
then fk1 c< fk by Th38;
then card fk1 < n-k by A3,A5,A4,CARD_2:48,XXREAL_0:2;
then card fk1 + 1 <= n-k by INT_1:7;
then card fk1 <= n-k-1 by XREAL_1:19;
hence card fk1 <= n-(k+1);
end;
hence thesis;
end;
A6: P[0]
proof
set f0=(repeat(R*M)).0 .f;
assume 0<=n;
card UnusedVx(f0,n) <= card Seg n by Th26,NAT_1:43;
hence thesis by FINSEQ_1:57;
end;
for k holds P[k] from NAT_1:sch 2(A6,A2);
then P[n];
then
A7: UnusedVx(nf,n) = {};
OuterVx(nf,n) c= UnusedVx(nf,n) by Th27;
hence contradiction by A1,A7,XBOOLE_1:3;
end;
Lm9: n-k <= n
proof
n <= n+k by NAT_1:11;
hence thesis by XREAL_1:20;
end;
Lm10: for p,q being FinSequence of NAT,f be Element of REAL*,i,n be Element of
NAT st (for k st 1<=k & k < len p holds p.(len p-k)=f.(p/.(len p-k+1)+n)) & (
for k st 1<=k & k < len q holds q.(len q-k)=f.(q/.(len q-k+1)+n)) & len p <=
len q & p.len p = q.len q holds for k st 1<=k & k < len p holds p.(len p-k)=q.(
len q-k)
proof
let p,q be FinSequence of NAT,f be Element of REAL*,i,n be Element of NAT;
assume that
A1: for k st 1<=k & k < len p holds p.(len p-k) =f.(p/.(len p-k+1)+n) and
A2: for k st 1<=k & k < len q holds q.(len q-k)=f.(q/.(len q-k+1)+n) and
A3: len p <= len q and
A4: p.len p = q.len q;
defpred P[Nat] means
$1 < len p implies p.(len p-$1)=q.(len q-$1);
A5: for k st P[k] holds P[k+1]
proof
let k;
assume
A6: P[k];
now
A7: k <= k+1 & len q-k <= len q by Lm9,NAT_1:11;
assume
A8: k+1 < len p;
then
A9: 1 <= len p-k by XREAL_1:19;
len p - k <= len q - k by A3,XREAL_1:9;
then
A10: 1 <= len q- k by A9,XXREAL_0:2;
A11: k+1 < len q by A3,A8,XXREAL_0:2;
A12: p/.(len p-k)=p.(len p-k) by A9,Lm9,Th3
.=q/.(len q-k) by A6,A8,A7,A10,Th3,XXREAL_0:2;
thus p.(len p-(k+1))=f.(p/.(len p-(k+1)+1)+n) by A1,A8,NAT_1:11
.=f.(q/.(len q-(k+1)+1)+n) by A12
.=q.(len q-(k+1)) by A2,A11,NAT_1:11;
end;
hence thesis;
end;
A13: P[0] by A4;
for k holds P[k] from NAT_1:sch 2(A13,A5);
hence thesis;
end;
theorem Th41:
dom f = dom ((repeat(Relax(n)*findmin(n))).i.f)
proof
set R=Relax(n), M=findmin(n);
defpred P[Nat] means dom f = dom ((repeat(R*M)).$1.f);
dom ((repeat(R*M)).0 .f)= dom ((id (REAL*)).f) by Def2
.= dom f;
then
A1: P[0];
A2: for k st P[k] holds P[k+1] by Th37;
for k holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
definition
let f,g be Element of REAL*,m,n be Nat;
pred f,g equal_at m,n means
dom f = dom g & for k st k in dom f & m <=k & k <= n holds f.k=g.k;
end;
theorem Th42:
f,f equal_at m,n;
theorem Th43:
f,g equal_at m,n & g,h equal_at m,n implies f,h equal_at m,n
proof
assume that
A1: f,g equal_at m,n and
A2: g,h equal_at m,n;
A3: dom f = dom g by A1;
A4: now
let k;
assume
A5: k in dom f & m <=k & k <= n;
hence f.k=g.k by A1
.=h.k by A2,A3,A5;
end;
dom g = dom h by A2;
hence thesis by A3,A4;
end;
theorem Th44:
(repeat(Relax(n)*findmin(n))).i.f, (repeat(Relax(n)*findmin(n)))
.(i+1).f equal_at 3*n+1,n*n+3*n
proof
set R=Relax(n), M=findmin(n), ff=(repeat (R*M)).i.f;
set Fi1=(repeat (R*M)).(i+1).f;
A1: now
let k;
assume that
A2: k in dom ff and
A3: 3*n+1 <= k and
A4: k <= n*n+3*n;
A5: k > 3*n by A3,NAT_1:13;
A6: k in dom (M.ff) by A2,Th33;
A7: k < n*n+3*n+1 by A4,NAT_1:13;
3*n >= n by Lm6;
then
A8: k > n by A5,XXREAL_0:2;
thus Fi1.k=(R.(M.ff)).k by Th22
.=(M.ff).k by A5,A6,Th36
.=ff.k by A7,A8,Th31;
end;
dom (Fi1) = dom ff by Th37;
hence thesis by A1;
end;
theorem
for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*, n,
i be Element of NAT st i < LifeSpan(F,f,n) holds OuterVx((repeat F).i.f,n) <>
{} by Def4;
theorem Th46:
f, (repeat(Relax(n)*findmin(n))).i.f equal_at 3*n+1,n*n+3*n
proof
set R=Relax(n), M=findmin(n), m=3*n+1, mm=n*n+3*n;
defpred P[Nat] means f,(repeat(R*M)).$1.f equal_at m,mm;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume
A2: P[k];
(repeat(R*M)).k.f, (repeat(R*M)).(k+1).f equal_at m,mm by Th44;
hence thesis by A2,Th43;
end;
(repeat(R*M)).0 .f =f by Th21;
then
A3: P[0] by Th42;
for k holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th47:
1<=n & 1 in dom f & f.(n+1) <> -1 & (for i st 1<=i & i<=n holds
f.i=1) & (for i st 2<=i & i<=n holds f.(n+i)=-1) implies 1 = Argmin(OuterVx(f,n
),f,n) & UsedVx(f,n)={} & {1} = UsedVx((repeat(Relax(n)*findmin(n))).1.f,n)
proof
set R=Relax(n), M=findmin(n), f0=(repeat (R*M)).0 .f, RT=repeat (R*M);
assume that
A1: 1<=n and
A2: 1 in dom f & f.(n+1) <> -1 and
A3: for i st 1<=i & i<=n holds f.i=1 and
A4: for i st 2<=i & i<=n holds f.(n+i)=-1;
set k=Argmin(OuterVx(f,n),f,n);
f.1=1 by A1,A3;
then
A5: 1 in {j: j in dom f & 1 <= j & j <= n & f.j <> -1 & f.(n+j) <> -1 } by A1
,A2;
thus
A6: k=1
proof
assume
A7: k<>1;
1<=k by A5,Th29;
then 1 < k by A7,XXREAL_0:1;
then
A8: 1+1 <= k by INT_1:7;
k<=n & f.(n+k) <> -1 by A5,Th29;
hence contradiction by A4,A8;
end;
thus
A9: UsedVx(f,n)={}
proof
assume UsedVx(f,n)<>{};
then consider x being object such that
A10: x in UsedVx(f,n) by XBOOLE_0:def 1;
ex j st x=j & j in dom f & 1 <= j & j <= n & f.j = -1 by A10;
hence contradiction by A3;
end;
OuterVx(f,n) <> {} by A5;
then
A11: OuterVx(f0,n) <> {} by Th21;
A12: Argmin(OuterVx(f0,n),f0,n) = Argmin(OuterVx(f,n),f0,n) by Th21
.=1 by A6,Th21;
thus UsedVx(RT.1.f,n) = UsedVx(RT.(0+1).f,n)
.=UsedVx(f0,n) \/ {1} by A11,A12,Th39
.= UsedVx(f,n) \/ {1} by Th21
.={1} by A9;
end;
theorem Th48:
g=(repeat(Relax(n)*findmin(n))).1.f & h=(repeat(Relax(n)*findmin
(n))).i.f & 1<=i & i <= LifeSpan(Relax(n)*findmin(n),f,n) & m in UsedVx(g,n)
implies m in UsedVx(h,n)
proof
set RF=Relax(n)*findmin(n), RT=repeat RF, cn=LifeSpan(RF,f,n);
assume that
A1: g=RT.1.f and
A2: h=RT.i.f & 1<=i & i <= cn and
A3: m in UsedVx(g,n);
defpred P[Nat] means
1<=$1 & $1<=cn implies m in UsedVx(RT.$1.f,n);
A4: for k st P[k] holds P[k+1]
proof
let k;
assume
A5: P[k];
hereby
assume that
1<=k+1 and
A6: k+1 <= cn;
per cases;
suppose
k=0;
hence m in UsedVx(RT.(k+1).f,n) by A1,A3;
end;
suppose
A7: k<>0;
k < cn by A6,NAT_1:13;
then OuterVx(RT.k.f,n) <> {} by Def4;
then
UsedVx(RT.(k+1).f,n)=UsedVx(RT.k.f,n) \/ {Argmin(OuterVx(RT.k.f,n
),RT.k.f,n)} by Th39;
then
A8: UsedVx(RT.k.f,n) c= UsedVx(RT.(k+1).f,n) by XBOOLE_1:7;
k >= 1+ 0 by A7,INT_1:7;
hence m in UsedVx(RT.(k+1).f,n) by A5,A6,A8,NAT_1:13;
end;
end;
end;
A9: P[0];
for k holds P[k] from NAT_1:sch 2(A9,A4);
hence thesis by A2;
end;
definition
let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat;
pred p is_vertex_seq_at f,i,n means
p.(len p)=i & for k st 1<=k & k
< len p holds p.(len p-k)=f.(n+p/.(len p-k+1));
end;
definition
let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat;
pred p is_simple_vertex_seq_at f,i,n means
p.1=1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one;
end;
theorem
for p,q being FinSequence of NAT,f be Element of REAL*,i,n be Element
of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n
holds p = q
proof
let p,q be FinSequence of NAT,f be Element of REAL*,i,n be Element of NAT;
assume that
A1: p is_simple_vertex_seq_at f,i,n and
A2: q is_simple_vertex_seq_at f,i,n;
A3: p.1=1 by A1;
A4: q.1=1 by A2;
A5: p is_vertex_seq_at f,i,n by A1;
then
A6: p.(len p)=i & for k st 1<=k & k < len p holds p.(len p-k)=f.(p/.(len p-k
+1)+ n);
A7: q is_vertex_seq_at f,i,n by A2;
then
A8: q.(len q)=i;
A9: for k st 1<=k & k < len q holds q.(len q-k)=f.(q/.(len q-k+1)+n) by A7;
A10: len p > 1 by A1;
A11: now
assume
A12: len p <> len q;
per cases;
suppose
A13: len p < len q;
A14: len p -1 > 1-1 by A10,XREAL_1:14;
then reconsider k=len p -1 as Element of NAT by INT_1:3;
A15: len p - k =0+1;
then
A16: len q - k > 1 by A13,XREAL_1:14;
then reconsider m=len q -k as Element of NAT by INT_1:3;
A17: k < len p by XREAL_1:146;
k >= 0+1 by A14,INT_1:7;
then
A18: 1=q.(len q-k) by A3,A6,A8,A9,A13,A15,A17,Lm10;
q is one-to-one & m <= len q by A2,Lm9;
hence contradiction by A4,A18,A16,GRAPH_5:6;
end;
suppose
A19: len p >= len q;
A20: p is one-to-one by A1;
A21: len p > len q by A12,A19,XXREAL_0:1;
hereby
per cases;
suppose
len q <=1;
hence contradiction by A2;
end;
suppose
len q > 1;
then
A22: len q -1 > 1-1 by XREAL_1:14;
then reconsider k=len q -1 as Element of NAT by INT_1:3;
A23: k < len q by XREAL_1:146;
A24: len q - k =0+1;
then
A25: len p - k > 1 by A21,XREAL_1:14;
then reconsider m=len p -k as Element of NAT by INT_1:3;
k >= 0+1 by A22,INT_1:7;
then
A26: 1=p.(len p-k) by A6,A4,A8,A9,A19,A24,A23,Lm10;
m <= len p by Lm9;
hence contradiction by A3,A20,A26,A25,GRAPH_5:6;
end;
end;
end;
end;
now
let k be Nat;
assume that
A27: 1 <=k and
A28: k <= len p;
per cases;
suppose
k=len p;
hence p.k=q.k by A5,A8,A11;
end;
suppose
k <> len p;
then k < len p by A28,XXREAL_0:1;
then
A29: len p-k > k-k by XREAL_1:14;
then reconsider m=len p-k as Element of NAT by INT_1:3;
A30: len q - m =0+k by A11;
len p - k <= len p -1 by A27,XREAL_1:13;
then
A31: m < len p by XREAL_1:146,XXREAL_0:2;
m >= 0+1 by A29,INT_1:7;
hence p.k=q.k by A6,A8,A9,A30,A31,Lm10;
end;
end;
hence thesis by A11,FINSEQ_1:14;
end;
definition
let G be Graph,p be FinSequence of the carrier' of G,vs be FinSequence;
pred p is_oriented_edge_seq_of vs means
len vs = len p + 1 & for n
be Nat st 1<=n & n<=len p holds (the Source of G).(p.n) = vs.n & (the Target of
G).(p.n) = vs.(n+1);
end;
theorem
for G being oriented Graph,vs be FinSequence,p,q being oriented Chain
of G st p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds p=q
proof
let G be oriented Graph,vs be FinSequence,p,q be oriented Chain of G;
assume that
A1: p is_oriented_edge_seq_of vs and
A2: q is_oriented_edge_seq_of vs;
A3: len p+1 = len vs by A1
.= len q +1 by A2;
now
let k be Nat;
assume
A4: 1<=k & k <= len p;
then
A5: (the Target of G).(p.k) = vs.(k+1) by A1
.=(the Target of G).(q.k) by A2,A3,A4;
A6: p.k in the carrier' of G & q.k in the carrier' of G by A3,A4,Th2;
(the Source of G).(p.k) = vs.k by A1,A4
.=(the Source of G).(q.k) by A2,A3,A4;
hence p.k=q.k by A5,A6,GRAPH_1:def 7;
end;
hence thesis by A3,FINSEQ_1:14;
end;
theorem
for G being Graph,vs1,vs2 be FinSequence,p being oriented Chain of G
st p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1
holds vs1=vs2
proof
let G be Graph,vs1,vs2 be FinSequence,p be oriented Chain of G;
assume that
A1: p is_oriented_edge_seq_of vs1 and
A2: p is_oriented_edge_seq_of vs2 and
A3: len p >= 1;
A4: now
let k be Nat;
assume that
A5: 1<=k and
A6: k <= len vs1;
per cases;
suppose
k = len vs1;
then
A7: k = len p + 1 by A1;
hence vs1.k=(the Target of G).(p.len p) by A1,A3
.=vs2.k by A2,A3,A7;
end;
suppose
k <> len vs1;
then k < len vs1 by A6,XXREAL_0:1;
then k+1 <= len vs1 by INT_1:7;
then k+1 <= len p+1 by A1;
then
A8: k <= len p by XREAL_1:6;
hence vs1.k=(the Source of G).(p.k) by A1,A5
.=vs2.k by A2,A5,A8;
end;
end;
len vs1 = len p+1 by A1
.= len vs2 by A2;
hence thesis by A4,FINSEQ_1:14;
end;
Lm11: 1<= i & i <= n implies 1 < 2*n+i & 2*n+i < n*n+3*n+1 & i < 2*n + i
proof
assume that
A1: 1<= i and
A2: i <= n;
set m2=2*n+i;
2*n+1 <= m2 by A1,XREAL_1:7;
then
A3: 2*n < m2 by NAT_1:13;
1 <= n by A1,A2,XXREAL_0:2;
then 2*1 <= 2*n by XREAL_1:64;
then 2 < m2 by A3,XXREAL_0:2;
hence 1 < m2 by XXREAL_0:2;
A4: 3*n < n*n+3*n+1 by Lm7;
2*n+n=(2+1)*n;
then m2 <= 3*n by A2,XREAL_1:7;
hence m2 < n*n+3*n+1 by A4,XXREAL_0:2;
n <= 2*n by Lm6;
then i <= 2*n by A2,XXREAL_0:2;
hence thesis by A3,XXREAL_0:2;
end;
Lm12: 1<= i & i <= n implies 1 < n+i & n+i <= 2*n & n+i < n*n+3*n+1
proof
assume that
A1: 1<= i and
A2: i <= n;
set ni=n+i;
1 <= n by A1,A2,XXREAL_0:2;
then 1+1 <= ni by A1,XREAL_1:7;
hence 1 < ni by NAT_1:13;
A3: ni <= n+n by A2,XREAL_1:7;
hence ni <= 2*n;
2*n < n*n+3*n+1 by Lm7;
hence thesis by A3,XXREAL_0:2;
end;
Lm13: 1 <= i & i <= n & j <= n implies 1 < 2*n+n*i+j & i < 2*n+n*i+j & 2*n+n*i
+j < n*n+3*n+1
proof
assume that
A1: 1<= i and
A2: i <= n and
A3: j<=n;
A4: 1 <= n by A1,A2,XXREAL_0:2;
then 2*1 <= 2*n by XREAL_1:64;
then
A5: 1 < 2*n by XXREAL_0:2;
set m3=2*n+n*i+j;
A6: m3 = 2*n+j+n*i & n*i <= n*n by A2,XREAL_1:64;
m3=2*n+(n*i+j);
then 2*n <= m3 by NAT_1:12;
hence 1 < m3 by A5,XXREAL_0:2;
A7: 2*n+n*i <= m3 by NAT_1:12;
1*i <= n*i by A4,XREAL_1:64;
then 1+i < 2*n+n*i by A5,XREAL_1:8;
then 1+i < m3 by A7,XXREAL_0:2;
hence i < m3 by NAT_1:13;
2*n+n=(2+1)*n;
then 2*n+j <= 3*n by A3,XREAL_1:7;
then m3 <= n*n+3*n by A6,XREAL_1:7;
hence thesis by NAT_1:13;
end;
Lm14: 1 <= i & i <= n & 1<=j & j <= n implies 3*n+1 <= 2*n+n*i+j & 2*n+n*i+j
<= n*n+3*n
proof
assume that
A1: 1<= i and
A2: i <= n and
A3: 1<=j and
A4: j<=n;
set m3=2*n+n*i+j;
A5: m3 = 2*n + j + n*i & n*i <= n*n by A2,XREAL_1:64;
n*1 <= n*i by A1,XREAL_1:64;
then 2*n + n <= 2*n +n*i by XREAL_1:7;
hence 3*n+1 <= m3 by A3,XREAL_1:7;
2*n+n=(2+1)*n;
then 2*n+j <= 3*n by A4,XREAL_1:7;
hence thesis by A5,XREAL_1:7;
end;
begin :: Data structure for Dijkstra's shortest path algorithm
:: address possible value init. value comment
:: 1 1 or -1 1 -1 if node v1 is used
:: 2 1 or -1 1 -1 if node v2 is used
:: : : : :
:: n 1 or -1 1 -1 if node vn is used
:: n+1 0 0 preceding-node of v1 toward v1
:: n+2 -1 or Node No. -1 preceding-node of v2 toward v1
:: : : : :
:: 2*n -1 or Node No. -1 preceding-node of vn toward v1
:: 2*n+1 0 0 cost from v1 to v1
:: 2*n+2 >=0 0 minimum cost from v2 to v1
:: : : : :
:: 3*n >=0 0 minimum cost from vn to v1
:: 3*n+1 weight(v1,v1) the weight of edge(v1,v1)
:: 3*n+2 weight(v1,v2) the weight of edge(v1,v2)
:: : : :
:: 4*n weight(v1,vn) the weight of edge(v1,vn)
:: : : :
:: n*n+3*n weight(vn,vn) the weight of edge(vn,vn)
:: n*n+3n+1 Node No. current node with the shortest path
definition
let f be Element of REAL*,G be oriented Graph,n be Nat, W be
Function of (the carrier' of G), Real>=0;
pred f is_Input_of_Dijkstra_Alg G,n,W means
len f=n*n+3*n+1 & Seg n=
the carrier of G & (for i st 1 <= i & i <= n holds f.i=1 & f.(2*n+i)=0) & f.(n+
1)=0 & (for i st 2 <= i & i <= n holds f.(n+i)=-1) & for i,j being Vertex of G,
k,m st k=i & m=j holds f.(2*n+n*k+m)=Weight(i,j,W);
end;
begin :: The definition of Dijkstra's shortest path algorithm
definition
let n be Nat;
func DijkstraAlgorithm n -> Element of Funcs(REAL*,REAL*) equals
while_do(
Relax(n)*findmin(n),n);
coherence;
end;
begin :: Justifying the correctness of Dijkstra's shortest path algorithm
reserve p,q for FinSequence of NAT,
G for finite oriented Graph,
P,Q,R for oriented Chain of G,
W for Function of (the carrier' of G), Real>=0,
v1,v2,v3, v4 for Vertex of G;
Lm15: f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & n >= 1 & h=(repeat(Relax(n)*
findmin(n))).1.f implies (for v3,j st v3<>v1 & v3=j & h.(n+j)<>-1 holds ex p,P
st p is_simple_vertex_seq_at h,j,n & (for i st 1<=i & i<len p holds p.i in
UsedVx(h,n)) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3,UsedVx(
h,n),W & cost(P,W)=h.(2*n+j) & (not v3 in UsedVx(h,n) implies P
islongestInShortestpath UsedVx(h,n),v1,W )) & (for m,j st h.(n+j) = -1 & 1<=j &
j<=n & m in UsedVx(h,n) holds f.(2*n+n*m+j) = -1) & for m st m in UsedVx(h,n)
holds h.(n+m) <> -1
proof
set R=Relax(n), M=findmin(n), f0=(repeat (R*M)).0 .f, mi=n*n+3*n+1;
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: v1=1 and
A3: n >= 1 and
A4: h=(repeat(Relax(n)*findmin(n))).1.f;
A5: len f=mi by A1;
set nk=n+1;
A6: 2*n+n=(2+1)*n;
A7: f.(n+1) =0 by A1;
A8: 1 <= mi by NAT_1:12;
then
A9: 1 in dom f by A5,FINSEQ_3:25;
A10: ( for j st 1<=j & j<=n holds f.j=1)& for j st 2<=j & j<=n holds f.(n+j)=
-1 by A1;
then
A11: {1} = UsedVx(h,n) by A3,A4,A7,A9,Th47;
h=(repeat (R*M)).(0+1).f by A4;
then h=R.(M.f0) by Th22;
then
A12: h=Relax(M.f0,n) by Def15;
A13: Seg n=the carrier of G by A1;
then reconsider VG=the carrier of G as non empty Subset of NAT by A3;
set Ak=Argmin(OuterVx(f,n),f,n);
A14: dom (M.f0) = dom f0 by Th33
.= dom f by Th21;
A15: 1 = Ak by A3,A7,A10,A9,Th47;
A16: M.f0= M.f by Th21
.= (f,mi):=(1,-jj) by A15,Def11;
then M.f0.1=-jj by A9,Th19;
then not M.f0 hasBetterPathAt n,1;
then
A17: not M.f0 hasBetterPathAt n,nk-'n by NAT_D:34;
A18: nk < mi by A3,Lm12;
A19: W is_weight>=0of G by GRAPH_5:def 13;
hereby
set w1=2*n+1;
let v3,j;
set nj=n+j;
assume that
A20: v3<>v1 and
A21: v3=j and
A22: h.(n+j)<>-1;
set m2=2*n+j;
A23: j in VG by A21;
then
A24: 1<=j by A13,FINSEQ_1:1;
then n+1 <= nj by XREAL_1:7;
then
A25: n < nj by NAT_1:13;
A26: j <= n by A13,A23,FINSEQ_1:1;
then
A27: 1 < m2 & m2 < mi by A24,Lm11;
j > 1 by A2,A20,A21,A24,XXREAL_0:1;
then j >= 1+1 by INT_1:7;
then
A28: f.nj=-1 by A1,A26;
A29: nj <= 2*n by A24,A26,Lm12;
A30: mi in dom f by A8,A5,FINSEQ_3:25;
then
A31: M.f0/.mi = M.f0.mi by A14,PARTFUN1:def 6
.=jj by A16,A27,A30,Th17;
A32: 1 < w1 & w1 < mi by A3,Lm11;
then w1 in dom f by A5,FINSEQ_3:25;
then
A33: M.f0/.(2*n+M.f0/.mi)=M.f0.w1 by A14,A31,PARTFUN1:def 6
.=f.w1 by A16,A32,Th18
.=0 by A1,A3;
A34: m2 <= 3*n by A6,A26,XREAL_1:7;
A35: 1 < nj & nj < mi by A24,A26,Lm12;
then
A36: nj in dom f by A5,FINSEQ_3:25;
(M.f0).nj = f.nj by A16,A35,Th18;
then
A37: M.f0 hasBetterPathAt n,(nj -' n) by A14,A12,A22,A29,A36,A25,A28,Def14;
2*n+1 <= m2 by A24,XREAL_1:7;
then
A38: 2*n < m2 by NAT_1:13;
set m3=2*n+n*1+j;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
reconsider p=<*1,jj*> as FinSequence of NAT;
A40: 1 < m3 & m3 < mi by A3,A26,Lm13;
then m3 in dom f by A5,FINSEQ_3:25;
then
A41: M.f0/.(2*n+n*(M.f0/.mi)+j)=M.f0.m3 by A14,A31,PARTFUN1:def 6
.=f.m3 by A16,A40,Th18
.=Weight(v1,v3,W) by A1,A2,A21;
A42: nj -' n=j by NAT_D:34;
then M.f0/.(2*n+n*(M.f0/.mi)+j) >= 0 by A37;
then consider e being set such that
A43: e in the carrier' of G and
A44: e orientedly_joins v1,v3 by A41,Th23;
reconsider pe= <*e*> as oriented Chain of G by A43,Th5;
A45: len pe = 1 by FINSEQ_1:40;
A46: len p = 2 by FINSEQ_1:44;
then
A47: p.(len p)=j;
A48: now
let k be Nat;
assume 1<=k & k<=len pe;
then
A49: k=1 by A45,XXREAL_0:1;
hence (the Source of G).(pe.k)=(the Source of G).e
.= p.k by A2,A44,A49,GRAPH_4:def 1;
thus (the Target of G).(pe.k)=(the Target of G).e by A49
.= p.(k+1) by A21,A44,A49,GRAPH_4:def 1;
end;
A50: h.nj=1 by A14,A12,A29,A36,A25,A37,A31,Def14;
now
let k;
assume that
A51: 1 <= k and
A52: k < len p;
k < 1+1 by A52,FINSEQ_1:44;
then k <= 1 by NAT_1:13;
then k=1 by A51,XXREAL_0:1;
hence p.(len p-k)=h.(n+p/.(len p-k+1)) by A50,A46,A47,FINSEQ_4:15;
end;
then
A53: p is_vertex_seq_at h,j,n by A47;
m2 -' 2*n = j & m2 in dom (M.f0) by A5,A14,A27,FINSEQ_3:25,NAT_D:34;
then
A54: Relax(M.f0,n).m2=newpathcost(M.f0,n,m2-'2*n) by A42,A37,A34,A38,Def14
.=0 + M.f0/.(2*n+n*(M.f0/.mi)+j) by A33,NAT_D:34;
take p,pe;
p is one-to-one by A2,A20,A21,FINSEQ_3:94;
hence p is_simple_vertex_seq_at h,j,n by A46,A53;
hereby
let i;
assume that
A55: 1<=i and
A56: i<len p;
i + 1 <= 1 + 1 by A46,A56,INT_1:7;
then i <= 1 by XREAL_1:6;
then i = 1 by A55,XXREAL_0:1;
hence p.i in UsedVx(h,n) by A11,TARSKI:def 1;
end;
len p = len pe + 1 by A45,FINSEQ_1:44;
hence pe is_oriented_edge_seq_of p by A48;
thus pe is_shortestpath_of v1,v3,UsedVx(h,n),W by A2,A11,A43,A44,Th14;
thus cost(pe,W)=W.(pe.1) by A19,A45,Th4,GRAPH_5:46
.=W.e
.=h.(2*n+j) by A12,A41,A54,A43,A44,Th25;
assume not v3 in UsedVx(h,n);
for v2 st v2 in UsedVx(h,n) & v2 <> v1 & not ex Q st Q
is_shortestpath_of v1,v2,UsedVx(h,n),W & cost(Q,W) <= cost(pe,W) holds
contradiction by A2,A11,TARSKI:def 1;
hence pe islongestInShortestpath UsedVx(h,n),v1,W by GRAPH_5:def 19;
end;
A57: 2*n < mi by Lm7;
A58: 2*1 <= 2*n by A3,XREAL_1:64;
1 < nk by A3,Lm12;
then
A59: nk in dom f by A5,A18,FINSEQ_3:25;
A60: n < nk by NAT_1:13;
nk <= 2*n by A3,Lm12;
then
A61: h.nk=M.f0.nk by A14,A12,A60,A59,A17,Def14
.=f0.nk by A18,A60,Th31
.=0 by A7,Th21;
A62: n*1 <= n*n by A3,XREAL_1:64;
hereby
A63: n < mi by Lm7;
let m,j;
assume that
A64: h.(n+j) = -1 and
A65: 1<=j and
A66: j <= n and
A67: m in UsedVx(h,n);
reconsider v2=j as Vertex of G by A13,A65,A66,FINSEQ_1:1;
A68: 3*n < mi by Lm7;
set m2=2*n+j;
m2 <= 3*n by A6,A66,XREAL_1:7;
then
A69: m2 < mi by A68,XXREAL_0:2;
2*n+1 <= m2 by A65,XREAL_1:7;
then 2*n < m2 by NAT_1:13;
then 2 < m2 by A58,XXREAL_0:2;
then
A70: 1 < m2 by XXREAL_0:2;
j <> 1 by A61,A64;
then
A71: M.f0.j=f.j by A16,A66,A63,Th18
.=1 by A1,A65,A66;
A72: mi in dom f by A8,A5,FINSEQ_3:25;
then
A73: M.f0/.mi = M.f0.mi by A14,PARTFUN1:def 6
.=1 by A16,A69,A70,A72,Th17;
set nj=n+j;
1+1 <= nj by A3,A65,XREAL_1:7;
then
A74: 1 < nj by NAT_1:13;
A75: nj <= n+n by A66,XREAL_1:7;
then nj < mi by A57,XXREAL_0:2;
then
A76: nj in dom f by A5,A74,FINSEQ_3:25;
n+1 <= nj by A65,XREAL_1:7;
then
A77: n < nj by NAT_1:13;
A78: nj <= 2*n by A75;
then
A79: not M.f0 hasBetterPathAt n,(nj-'n) by A14,A12,A64,A76,A77,A73,Def14;
then nj -' n=j & M.f0.nj=-1 by A14,A12,A64,A78,A76,A77,Def14,NAT_D:34;
then
A80: not M.f0/.(2*n+n*(M.f0/.mi)+j) >= 0 by A79,A71;
set m3=2*n+n*1+j;
m3 = 2*n+(n*1+j);
then 2 <= m3 by A58,NAT_1:12;
then
A81: 1 < m3 by XXREAL_0:2;
j <= n*n by A62,A66,XXREAL_0:2;
then m3 <= 3*n + n*n by XREAL_1:7;
then
A82: m3 < mi by NAT_1:13;
then m3 in dom f by A5,A81,FINSEQ_3:25;
then
A83: M.f0/.(2*n+n*(M.f0/.mi)+j)=M.f0.m3 by A14,A73,PARTFUN1:def 6;
M.f0.m3=f.m3 by A16,A81,A82,Th18
.=Weight(v1,v2,W) by A1,A2;
then not ex e be set st e in the carrier' of G & e orientedly_joins v1,
v2 by A80,A83,Th23;
then
A84: Weight(v1,v2,W)=-1 by Def7;
m=1 by A11,A67,TARSKI:def 1;
hence f.(2*n+n*m+j) = -1 by A1,A2,A84;
end;
let m;
assume m in UsedVx(h,n);
then m=1 by A11,TARSKI:def 1;
hence thesis by A61;
end;
Lm16: g =(repeat(Relax(n)*findmin(n))).k.f & h=(repeat(Relax(n)*findmin(n))).(
k+1).f & OuterVx(g,n) <> {} & i in UsedVx(g,n) & len f=n*n+3*n+1 implies h.(n+i
)=g.(n+i)
proof
set R=Relax(n), M=findmin(n), RF=repeat (R*M);
set mi=n*n+3*n+1, Ak=Argmin(OuterVx(g,n),g,n);
assume that
A1: g=RF.k.f and
A2: h=RF.(k+1).f and
A3: OuterVx(g,n) <> {} and
A4: i in UsedVx(g,n) and
A5: len f= mi;
A6: h=R.(M.g) by A1,A2,Th22
.=Relax(M.g,n) by Def15;
set ni=n+i;
A7: ex j st i=j & j in dom g & 1 <= j & j <= n & g.j = -1 by A4;
then
A8: ni <= n+n by XREAL_1:7;
A9: 1 <= ni by A7,NAT_1:12;
A10: 2*n < mi by Lm7;
then ni < mi by A8,XXREAL_0:2;
then ni in dom f by A5,A9,FINSEQ_3:25;
then ni in dom g by A1,Th41;
then
A11: ni -' n=i & ni in dom (M.g) by Th33,NAT_D:34;
A12: Ak<=n by A3,Th29;
A13: n < mi by Lm7;
A14: M.g= (g,mi):=(Ak,-jj) by Def11;
g.Ak <> -1 by A3,Th29; then
A15: not M.g hasBetterPathAt n,i by A14,A7,A13,Th18;
n+1 <= ni by A7,XREAL_1:7;
then
A16: n < ni by NAT_1:13;
ni <= 2*n by A8;
hence h.ni=M.g.ni by A6,A16,A11,A15,Def14
.=g.ni by A14,A12,A8,A16,A10,Th18;
end;
Lm17: g =(repeat(Relax(n)*findmin(n))).k.f & h=(repeat(Relax(n)*findmin(n))).(
k+1).f & OuterVx(g,n) <> {} & len f=n*n+3*n+1 & p is_simple_vertex_seq_at g,j,n
& g.(n+j)=h.(n+j) & (for i st 1<=i & i<len p holds p.i in UsedVx(g,n)) implies
p is_simple_vertex_seq_at h,j,n
proof
set RT=repeat(Relax(n)*findmin(n));
assume that
A1: g=RT.k.f & h=RT.(k+1).f & OuterVx(g,n) <> {} & len f=n*n+3*n+1 and
A2: p is_simple_vertex_seq_at g,j,n and
A3: g.(n+j)=h.(n+j) and
A4: for i st 1<=i & i<len p holds p.i in UsedVx(g,n);
A5: len p > 1 by A2;
A6: p is_vertex_seq_at g,j,n by A2;
then
A7: p.(len p)=j;
now
let k;
assume that
A8: 1<=k and
A9: k < len p;
A10: k - k < len p - k by A9,XREAL_1:14;
then reconsider m=len p - k as Element of NAT by INT_1:3;
m <= len p - 1 by A8,XREAL_1:13;
then
A11: m +1 <= len p-1+1 by XREAL_1:7;
A12: 1+0 < m + 1 by A10,XREAL_1:8;
then
A13: p/.(m+1)=p.(m+1) by A11,FINSEQ_4:15;
per cases;
suppose
m+1=len p;
hence p.(len p-k)=h.(n+p/.(len p-k+1)) by A3,A5,A6,A13;
end;
suppose
m+1<>len p;
then
A14: m+1 < len p by A11,XXREAL_0:1;
thus p.(len p-k)=g.(n+p/.(len p-k+1)) by A6,A8,A9
.=h.(n+p/.(len p-k+1)) by A1,A4,A12,A13,A14,Lm16;
end;
end;
then
A15: p is_vertex_seq_at h,j,n by A7;
p.1=1 & p is one-to-one by A2;
hence thesis by A5,A15;
end;
Lm18: g =(repeat(Relax(n)*findmin(n))).k.f & h=(repeat(Relax(n)*findmin(n))).(
k+1).f & OuterVx(g,n) <> {} & len f=n*n+3*n+1 & p is_simple_vertex_seq_at g,m,n
& m=h.(n+j) & g.(n+m)=h.(n+m) & m<>j & not j in UsedVx(g,n) & (for i st 1<=i &
i<len p holds p.i in UsedVx(g,n)) implies
for q being FinSequence of NAT st q = p^<*j*>
holds q is_simple_vertex_seq_at h,j,n
proof
set RT=repeat(Relax(n)*findmin(n));
assume that
A1: g=RT.k.f & h=RT.(k+1).f & OuterVx(g,n) <> {} & len f=n*n+3*n+1 and
A2: p is_simple_vertex_seq_at g,m,n and
A3: m=h.(n+j) and
A4: g.(n+m)=h.(n+m) and
A5: m<>j and
A6: not j in UsedVx(g,n) and
A7: for i st 1<=i & i<len p holds p.i in UsedVx(g,n);
A8: p is_vertex_seq_at g,m,n by A2;
then
A9: p.(len p)=m;
let q be FinSequence of NAT such that
A10: q=p^<*j*>;
A11: len p > 1 by A2;
A12: len q=len p+ 1 by FINSEQ_2:16,A10;
then
A13: q.(len q)=j by FINSEQ_1:42,A10;
now
let ii be Nat;
assume that
A14: 1<=ii and
A15: ii < len q;
A16: ii - ii < len q - ii by A15,XREAL_1:14;
then reconsider mm=len q - ii as Element of NAT by INT_1:3;
A17: 1+0 < mm + 1 by A16,XREAL_1:8;
mm <= len q - 1 by A14,XREAL_1:13;
then
A18: mm +1 <= len q-1+1 by XREAL_1:7;
then
A19: q/.(mm+1)=q.(mm+1) by A17,FINSEQ_4:15;
per cases;
suppose
mm+1=len q;
hence q.(len q-ii)=h.(n+q/.(len q-ii+1)) by A3,A11,A9,A12,A13,A19,Lm1,A10
;
end;
suppose
mm+1<>len q;
then
A20: mm+1 < len q by A18,XXREAL_0:1;
then
A21: mm+1 <= len p by A12,INT_1:7;
A22: 1+0 <= mm by A16,INT_1:7;
mm < len p by A12,A20,XREAL_1:7;
then
A23: q.(len q-ii)=p.mm by A22,Lm1,A10;
hereby
per cases;
suppose
A24: mm+1=len p;
A25: p/.(len p-1+1)=m by A11,A9,FINSEQ_4:15;
q/.(len q-ii+1)=m by A11,A9,A19,A24,Lm1,A10;
hence q.(len q-ii)=h.(n+q/.(len q-ii+1)) by A4,A11,A8,A23,A24,A25;
end;
suppose
A26: mm+1<>len p;
set i2=ii-1;
A27: mm+1 < len p by A21,A26,XXREAL_0:1;
A28: now
assume i2 <= 1;
then len p - 1 <= len p -i2 by XREAL_1:13;
hence contradiction by A12,A27,XREAL_1:20;
end;
then reconsider i3=i2 as Element of NAT by INT_1:3;
A29: p/.(mm+1)=p.(mm+1) by A17,A21,FINSEQ_4:15;
A30: q/.(len q-ii+1)= q.(mm+1) by A17,A18,FINSEQ_4:15
.=p/.(mm+1) by A17,A21,A29,Lm1,A10;
i2 < len q -1 by A15,XREAL_1:14;
hence q.(len q-ii) = g.(n+p/.(len p-i3+1)) by A8,A12,A23,A28
.=h.(n+q/.(len q-ii+1)) by A1,A7,A12,A17,A27,A29,A30,Lm16;
end;
end;
end;
end;
then
A31: q is_vertex_seq_at h,j,n by A13;
A32: now
assume j in rng p;
then consider i being Nat such that
A33: i in dom p and
A34: j = p.i by FINSEQ_2:10;
A35: 1<=i by A33,FINSEQ_3:25;
A36: i <= len p by A33,FINSEQ_3:25;
per cases;
suppose
i = len p;
hence contradiction by A5,A8,A34;
end;
suppose
i <> len p;
then i < len p by A36,XXREAL_0:1;
hence contradiction by A6,A7,A34,A35;
end;
end;
p is one-to-one by A2;
then
A37: q is one-to-one by A32,Th1,A10;
p.1=1 by A2;
then
A38: q.1=1 by A11,Lm1,A10;
len q > 1 by A11,A12,NAT_1:13;
hence thesis by A38,A31,A37;
end;
Lm19: f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2=i & v1<>v2 &
1<=i & i<=n & P is_shortestpath_of v1,v2,V,W & (for m,j st g.(n+j) = -1 & 1<=j
& j<=n & m in V holds f.(2*n+n*m+j) = -1) implies g.(n+i) <> -1
proof
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: W is_weight>=0of G and
A3: v2=i and
A4: v1<>v2 and
A5: 1<=i & i<=n and
A6: P is_shortestpath_of v1,v2,V,W and
A7: for m,j st g.(n+j) = -1 & 1<=j & j<=n & m in V holds f.(2*n+n*m+j)= -1;
P is_orientedpath_of v1,v2,V by A6,GRAPH_5:def 18;
then consider q being Simple oriented Chain of G such that
A8: q is_shortestpath_of v1,v2,V,W by A2,GRAPH_5:62;
set FT=the Target of G;
assume
A9: g.(n+i)=-1;
set e=q.len q;
consider vs being FinSequence of the carrier of G such that
A10: vs is_oriented_vertex_seq_of q and
A11: for n1,m1 be Nat st 1<=n1 & n1<m1 & m1<=len vs & vs.n1=
vs .m1 holds n1=1 & m1=len vs by GRAPH_4:def 7;
A12: q is_orientedpath_of v1,v2,V by A8,GRAPH_5:def 18;
then
A13: q is_orientedpath_of v1,v2 by GRAPH_5:def 4;
then q <> {} by GRAPH_5:def 3;
then
A14: len q >= 1 by FINSEQ_1:20;
then
A15: e orientedly_joins vs/.len q, vs/.(len q+1) by A10,GRAPH_4:def 5;
len q in dom q by A14,FINSEQ_3:25;
then
A16: e in the carrier' of G by FINSEQ_2:11;
A17: len vs = len q + 1 by A10,GRAPH_4:def 5;
then
A18: len q < len vs by NAT_1:13;
then
A19: len q in dom vs by A14,FINSEQ_3:25;
A20: vs/.len q=vs.len q by A14,A18,FINSEQ_4:15;
then reconsider v3=vs.len q as Vertex of G;
FT.(q.(len q))= v2 by A13,GRAPH_5:def 3;
then
A21: v2=vs/.(len q+1) by A15,GRAPH_4:def 1;
A22: 1 < len q+1 by A14,NAT_1:13;
then
A23: v2=vs.len vs by A17,A21,FINSEQ_4:15;
now
A24: q.1 orientedly_joins vs/.1, vs/.(1+1) by A10,A14,GRAPH_4:def 5;
assume
A25: v3=v2;
v1 =(the Source of G).(q.1) by A13,GRAPH_5:def 3
.=vs/.1 by A24,GRAPH_4:def 1
.=vs.1 by A17,A22,FINSEQ_4:15
.=v3 by A11,A14,A18,A23,A25;
hence contradiction by A4,A25;
end;
then
A26: not v3 in {v2} by TARSKI:def 1;
Seg n=the carrier of G by A1;
then v3 in Seg n by A19,FINSEQ_2:11;
then reconsider m=v3 as Element of NAT;
A27: f.(2*n+n*m+i)=Weight(v3,v2,W) by A1,A3;
v3=(the Source of G).e by A15,A20,GRAPH_4:def 1;
then v3 in vertices(q) by A14,Lm4;
then
A28: m in (vertices(q) \ {v2}) by A26,XBOOLE_0:def 5;
vertices(q) \ {v2} c= V by A12,GRAPH_5:def 4;
then f.(2*n+n*m+i)=-1 by A5,A7,A9,A28;
hence contradiction by A15,A16,A20,A21,A27,Th23;
end;
Lm20: f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & n >= 1 & g=(repeat(Relax(n)*
findmin(n))).k.f & h=(repeat(Relax(n)*findmin(n))).(k+1).f & OuterVx(g,n) <> {}
& 1 in UsedVx(g,n) & (for v3,j st v3<>v1 & v3=j & g.(n+j)<>-1 holds ex p,P st p
is_simple_vertex_seq_at g,j,n &(for i st 1<=i & i<len p holds p.i in UsedVx(g,n
)) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3,UsedVx(g,n),W &
cost(P,W)=g.(2*n+j) & (not v3 in UsedVx(g,n) implies P islongestInShortestpath
UsedVx(g,n),v1,W)) & (for m,j st g.(n+j) = -1 & 1<=j & j<=n & m in UsedVx(g,n)
holds f.(2*n+n*m+j) = -1) & (for m st m in UsedVx(g,n) holds g.(n+m) <> -1)
implies (for v3,j st v3<>v1 & v3=j & h.(n+j)<>-1 holds ex p,P st p
is_simple_vertex_seq_at h,j,n & (for i st 1<=i & i<len p holds p.i in UsedVx(h,
n)) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx(h,n),W &
cost(P,W)=h.(2*n+j) & (not v3 in UsedVx(h,n) implies P islongestInShortestpath
UsedVx(h,n),v1,W )) & (for m,j st h.(n+j) = -1 & 1<=j & j<=n & m in UsedVx(h,n)
holds f.(2*n+n*m+j) = -1) & for m st m in UsedVx(h,n) holds h.(n+m) <> -1
proof
set R=Relax(n), M=findmin(n), IN=OuterVx(g,n), Ug=UsedVx(g,n);
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and A2: v1=1
and A3: n >= 1
and A4: g=(repeat(R*M)).k.f
and A5: h=(repeat(R*M)).(k+1).f
and A6: IN <> {}
and A7: 1 in Ug ;
assume
A8: for v3,j st v3<>v1 & v3=j & g.(n+j)<>-1 holds ex p,P st p
is_simple_vertex_seq_at g,j,n & (for i st 1<=i & i<len p holds
p.i in Ug) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3,
Ug,W & cost(P,W)=g.(2*n+j) & (not v3 in Ug implies
P islongestInShortestpath Ug,v1,W);
assume that
A9: for m,j st g.(n+j) = -1 & 1<=j & j<=n & m in Ug holds f.(2*n+n*m+j) = - 1
and A10: for m st m in UsedVx(g,n) holds g.(n+m) <> -1 ;
set mi=n*n+3*n+1, Ak=Argmin(IN,g,n);
A11: 1 <= mi by NAT_1:12;
A12: len f=mi by A1;
A13: M.g= (g,mi):=(Ak,-jj) by Def11;
A14: dom (M.g) = dom g by Th33;
h=R.(M.g) by A4,A5,Th22;
then A15: h=Relax(M.g,n) by Def15;
A16: Seg n=the carrier of G by A1;
then reconsider VG=the carrier of G as non empty Subset of NAT by A3;
A17: W is_weight>=0of G by GRAPH_5:def 13;
A18: 2*n+n=(2+1)*n;
A19: dom f=dom g by A4,Th41;
A20: 1<=Ak by A6,Th29;
A21: Ak<=n by A6,Th29;
A22: g.(n+Ak) <> -1 by A6,Th29;
set Uh=UsedVx(h,n);
A23: Uh=Ug \/ {Ak} & not Ak in Ug by A4,A5,A6,Th39;
then A24: Ug c= Uh by XBOOLE_1:7;
A25: n < mi by Lm7;
A26: dom f=dom h by A5,Th41;
reconsider vk=Ak as Vertex of G by A16,A20,A21,FINSEQ_1:1;
consider pk being FinSequence of NAT,PK be oriented Chain of G such that
A27: pk is_simple_vertex_seq_at g,Ak,n
and A28: for i st 1<=i & i<len pk holds pk.i in Ug
and A29: PK is_oriented_edge_seq_of pk
and A30: PK is_shortestpath_of v1,vk,Ug,W
and A31: cost(PK,W)=g.(2*n+Ak)
and A32: not vk in Ug implies PK islongestInShortestpath Ug,v1,W by A2,A7
,A8,A22,A23;
A33:ex kk being Nat st ( kk=Ak)&( kk in IN)&( for i
st i in IN holds g/.(2*n+kk) <= g/.(2*n+i))&( for i st i in IN & g/.(2*n+kk) =
g/.(2*n+i) holds kk <= i) by A6,Def10;
set nAk=2*n+Ak;
A34: 1 < nAk by A20,A21,Lm11;
A35: nAk < mi by A20,A21,Lm11;
A36: Ak < nAk by A20,A21,Lm11;
A37: nAk in dom g by A12,A19,A34,A35,FINSEQ_3:25;
A38: f,g equal_at 3*n+1,n*n+3*n by A4,Th46;
PK is_orientedpath_of v1,vk,Ug by A30,GRAPH_5:def 18;
then A39: PK is_orientedpath_of v1,vk by GRAPH_5:def 4;
then PK <> {} by GRAPH_5:def 3;
then A40: len PK >= 1 by FINSEQ_1:20;
A41: mi in dom g by A11,A12,A19,FINSEQ_3:25;
then A42: M.g/.mi = M.g.mi by A14,PARTFUN1:def 6
.=Ak by A13,A21,A25,A41,Th17;
A43: M.g/.nAk=M.g.nAk by A14,A37,PARTFUN1:def 6
.=cost(PK,W) by A13,A31,A35,A36,Th18;
set nk=n+Ak;
A44: 1 < nk by A20,A21,Lm12;
A45: nk <= 2*n by A20,A21,Lm12;
A46: nk < mi by A20,A21,Lm12;
n+1 <= nk by A20,XREAL_1:7;
then A47: n < nk by NAT_1:13;
A48: nk in dom g by A12,A19,A44,A46,FINSEQ_3:25;
A49: M.g.nk=g.nk by A46,A47,Th31;
now
set Wke=M.g/.(2*n+n*(M.g/.mi)+Ak);
assume A50: M.g hasBetterPathAt n,Ak;
then A51: M.g.nk=-1 or M.g/.nAk > newpathcost(M.g,n,Ak);
Wke >= 0 by A50;
then M.g/.nAk+Wke >= M.g/.nAk+0 by XREAL_1:7;
hence contradiction by A6,A42,A49,A51,Th29;
end;
then not M.g hasBetterPathAt n,nk-'n by NAT_D:34;
then A52: h.nk=g.nk by A14,A15,A45,A47,A48,A49,Def14;
hereby
let v3,j;
assume that
A53: v3<>v1 and A54: v3=j
and A55: h.(n+j)<>-1 ;
set nj=n+j;
A56: j in VG by A54;
then A57: 1<=j by A16,FINSEQ_1:1;
A58: j <= n by A16,A56,FINSEQ_1:1;
then A59: 1 < nj by A57,Lm12;
A60: nj <= 2*n by A57,A58,Lm12;
A61: nj < mi by A57,A58,Lm12;
then A62: nj in dom g by A12,A19,A59,FINSEQ_3:25;
A63: nj -' n=j by NAT_D:34;
n+1 <= nj by A57,XREAL_1:7;
then A64: n < nj by NAT_1:13;
set m2=2*n+j;
A65: m2 <= 3*n by A18,A58,XREAL_1:7;
2*n+1 <= m2 by A57,XREAL_1:7;
then A66: 2*n < m2 by NAT_1:13;
A67: m2 -' 2*n = j by NAT_D:34;
A68: 1 < m2 by A57,A58,Lm11;
A69: m2 < mi by A57,A58,Lm11;
then A70: m2 in dom g by A12,A19,A68,FINSEQ_3:25;
A71: m2 in dom (M.g) by A12,A14,A19,A68,A69,FINSEQ_3:25;
A72: M.g.nj = g.nj by A13,A21,A61,A64,Th18;
n <= 2*n by Lm6;
then n < m2 by A66,XXREAL_0:2;
then A73: M.g.m2 = g.m2 by A13,A21,A69,Th18;
A74: j < mi by A25,A58,XXREAL_0:2;
then A75: j in dom g by A12,A19,A57,FINSEQ_3:25;
A76: j in dom h by A12,A26,A57,A74,FINSEQ_3:25;
set Akj=2*n+n*Ak+j;
A77: 1 < Akj by A20,A21,A58,Lm13;
A78: Ak < Akj by A20,A21,A58,Lm13;
A79: Akj < mi by A20,A21,A58,Lm13;
then A80: Akj in dom g by A12,A19,A77,FINSEQ_3:25;
A81: 3*n+1 <=Akj by A20,A21,A57,A58,Lm14;
A82: Akj <= n*n+3*n by A20,A21,A57,A58,Lm14;
A83: M.g/.(2*n+n*(M.g/.mi)+j)=M.g.Akj by A14,A42,A80,PARTFUN1:def 6
.=g.Akj by A13,A78,A79,Th18
.=f.Akj by A38,A80,A81,A82
.=Weight(vk,v3,W) by A1,A54;
A84: M.g/.m2 = g.m2 by A14,A70,A73,PARTFUN1:def 6;
per cases;
suppose
A85: not M.g hasBetterPathAt n,(nj-'n);
then A86: h.nj=g.nj by A14,A15,A60,A62,A64,A72,Def14;
then consider p,P such that
A87: p is_simple_vertex_seq_at g,j,n
and A88: for i st 1<=i & i<len p holds p.i in Ug
and A89: P is_oriented_edge_seq_of p
and A90: P is_shortestpath_of v1,v3,Ug,W
and A91: cost(P,W)=g.m2
and A92: not v3 in Ug implies P islongestInShortestpath Ug,v1,W
by A8,A53,A54,A55;
take p,P;
thus p is_simple_vertex_seq_at h,j,n by A4,A5,A6,A12,A86,A87,A88,Lm17;
thus for i st 1<=i & i<len p holds p.i in Uh by A24,A88;
thus P is_oriented_edge_seq_of p by A89;
hereby
per cases;
suppose M.g.j=-1;
then Relax(M.g,n).j=-1 by A14,A58,A75,Def14;
then j in {i: i in dom h & 1 <= i & i <= n & h.i = -1}
by A15,A57,A58,A76;
then A93: j in Ug or j in {Ak} by A23,XBOOLE_0:def 3;
now
let Q,v4;
assume that
A94: not v4 in Ug and A95: Q is_shortestpath_of v1,v4,Ug,W ;
A96: v4 in VG;
then reconsider j4=v4 as Element of NAT;
A97: 1<=j4 by A16,A96,FINSEQ_1:1;
A98: j4<=n by A16,A96,FINSEQ_1:1;
then
A99: g.(n+j4) <> -1 by A1,A2,A7,A9,A17,A94,A95,A97,Lm19;
then consider q,R such that
q is_simple_vertex_seq_at g,j4,n
and for i st 1<=i & i<len q holds q.i in Ug
and R is_oriented_edge_seq_of q
and A100: R is_shortestpath_of v1,v4,Ug,W
and A101: cost(R,W)=g.(2*n+j4)
and A102: not v4 in Ug implies R islongestInShortestpath Ug,v1,W
by A2,A7,A8,A94;
A103: cost(R,W)=cost(Q,W) by A95,A100,Th9;
per cases by A93,TARSKI:def 1;
suppose j in Ug;
then ex PP being oriented Chain of G st ( PP is_shortestpath_of
v1,v3,Ug,W)&( cost(PP,W) <= cost(R,W)) by A53,A54,A94,A102,GRAPH_5:def 19;
hence cost(P,W) <= cost(Q,W) by A90,A103,Th9;
end;
suppose
A104: j = Ak;
j4 <= mi by A25,A98,XXREAL_0:2;
then A105: j4 in dom g by A12,A19,A97,FINSEQ_3:25;
then g.j4<>-1 by A94,A97,A98;
then j4 in {i: i in dom g & 1 <= i & i <= n & g.i <> -1 &
g.(n+i) <> -1} by A97,A98,A99,A105;
then A106: g/.(2*n+Ak) <= g/.(2*n+j4) by A33;
A107: g/.(2*n+Ak) = g.(2*n+Ak) by A37,PARTFUN1:def 6;
A108: 1 < 2*n+j4 by A97,A98,Lm11;
2*n+j4 < mi by A97,A98,Lm11;
then 2*n+j4 in dom g by A12,A19,A108,FINSEQ_3:25;
hence cost(P,W) <= cost(Q,W)
by A91,A101,A103,A104,A106,A107,PARTFUN1:def 6;
end;
end;
hence P is_shortestpath_of v1,v3,Uh,W by A17,A24,A53,A90,GRAPH_5:64;
end;
suppose
A109: M.g.j <> -1;
hereby
per cases;
suppose
A110: M.g/.(2*n+n*(M.g/.mi)+j) >= 0;
then
A111: M.g/.m2 <= newpathcost(M.g,n,j) by A63,A85,A109;
A112: M.g/.m2 = cost(P,W) by A71,A73,A91,PARTFUN1:def 6;
consider e be set such that
A113: e in the carrier' of G and A114: e orientedly_joins vk,v3
by A83,A110,Th23;
reconsider pe= <*e*> as oriented Chain of G by A113,Th5;
A115: len pe = 1 by FINSEQ_1:40;
pe.1=e;
then consider Q such that
A117: Q=PK^pe
and Q is_orientedpath_of v1,v3 by A39,A40,A114,A115,GRAPH_5:33;
cost(pe,W) = W.(pe.1) by A17,A115,Th4,GRAPH_5:46
.=Weight(vk,v3,W) by A113,A114,Th25;
then
cost(Q,W)=newpathcost(M.g,n,j) by A17,A42,A43,A83,A117,GRAPH_5:46,54;
hence P is_shortestpath_of v1,v3,Uh,W
by A2,A7,A17,A23,A30,A32,A40,A53,A90,A111,A112,A113,A114,A117,
GRAPH_5:65;
end;
suppose M.g/.(2*n+n*(M.g/.mi)+j) < 0;
then not ex e be set st e in the carrier' of G &
e orientedly_joins vk,v3 by A83,Th23;
hence P is_shortestpath_of v1,v3,Uh,W
by A2,A7,A17,A23,A30,A32,A53,A90,Th13;
end;
end;
end;
end;
thus cost(P,W)=h.m2 by A15,A63,A65,A66,A67,A71,A73,A85,A91,Def14;
hereby
assume
A118: not v3 in Uh;
then A119: not v3 in Ug by A23,XBOOLE_0:def 3;
now
let v2;
assume that
A120: v2 in Uh and A121: v2 <> v1 ;
per cases by A23,A120,XBOOLE_0:def 3;
suppose v2 in {Ak};
then A122: v2 = vk by TARSKI:def 1;
take PK;
thus PK is_shortestpath_of v1,v2,Uh,W by A23,A30,A122,Th8;
g.j <> -1 by A54,A57,A58,A75,A119;
then j in {i: i in dom g & 1 <= i & i <= n & g.i <> -1 &
g.(n+i) <> -1} by A55,A57,A58,A75,A86;
then A123: g/.nAk <= g/.m2 by A33;
g/.nAk=cost(PK,W) by A31,A37,PARTFUN1:def 6;
hence
cost(PK,W) <= cost(P,W) by A70,A91,A123,PARTFUN1:def 6;
end;
suppose
A124: v2 in Ug;
then consider Q such that
A125: Q is_shortestpath_of v1,v2,Ug,W and A126: cost(Q,W) <= cost(P,W)
by A23,A92,A118,A121,GRAPH_5:def 19,XBOOLE_0:def 3;
A127: now
let R,v4;
assume that
A128: not v4 in Ug and A129: R is_shortestpath_of v1,v4,Ug,W ;
A130: v4 in VG;
then reconsider j4=v4 as Element of NAT;
A131: 1<=j4 by A16,A130,FINSEQ_1:1;
j4<=n by A16,A130,FINSEQ_1:1;
then
g.(n+j4) <> -1 by A1,A2,A7,A9,A17,A128,A129,A131,Lm19;
then consider rn being FinSequence of NAT,RR
be oriented Chain of G such that
rn is_simple_vertex_seq_at g,j4,n
and for i st 1<=i & i<len rn holds rn.i in Ug
and RR is_oriented_edge_seq_of rn
and A132: RR is_shortestpath_of v1,v4,Ug,W
and cost(RR,W) =g.(2*n+j4)
and A133: not v4 in Ug implies RR islongestInShortestpath Ug,v1,W
by A2,A7,A8,A128;
consider QQ being oriented Chain of G such that
A134: QQ is_shortestpath_of v1,v2,Ug,W
and A135: cost(QQ,W) <= cost(RR,W) by A121,A124,A128,A133,GRAPH_5:def 19;
cost(QQ,W)= cost(Q,W) by A125,A134,Th9;
hence cost(Q,W) <= cost(R,W) by A129,A132,A135,Th9;
end;
take Q;
thus Q is_shortestpath_of v1,v2,Uh,W
by A17,A24,A121,A125,A127,GRAPH_5:64;
thus cost(Q,W) <= cost(P,W) by A126;
end;
end;
hence P islongestInShortestpath Uh,v1,W by GRAPH_5:def 19;
end;
end;
suppose
A136: M.g hasBetterPathAt n,(nj-'n);
then A137: Relax(M.g,n).nj=Ak by A14,A42,A60,A62,A64,Def14;
A138: M.g.nj=-1 or M.g/.m2 > newpathcost(M.g,n,j) by A63,A136;
A139: M.g/.(2*n+n*(M.g/.mi)+j) >= 0 by A63,A136;
A140: M.g.j <> -1 by A63,A136;
A141: newpathcost(M.g,n,j) =M.g/.nAk+Weight(vk,v3,W) by A42,A83;
A142: now
assume
A143: Ak = j;
then A144: M.g.nj <> -1 by A13,A21,A22,A61,A64,Th18;
M.g/.m2+Weight(vk,v3,W) >= M.g/.m2+0 by A83,A139,XREAL_1:7;
hence contradiction by A63,A136,A141,A143,A144;
end;
A145: now
assume j in UsedVx(g,n);
then
ex i st ( j=i)&( i in dom g)&( 1 <= i)&( i <= n)&( g.i = -1 );
hence contradiction by A25,A140,Th32;
end;
consider e being set such that
A146: e in the carrier' of G & e orientedly_joins vk,v3 by A83,A139,Th23;
reconsider pe= <*e*> as oriented Chain of G by A146,Th5;
A147: len pe = 1 by FINSEQ_1:40;
A148: pe.1=e;
then consider Q such that
A149: Q=PK^pe
and Q is_orientedpath_of v1,v3 by A39,A40,A146,A147,GRAPH_5:33;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
reconsider q=pk^<*jj*> as FinSequence of NAT;
take q,Q;
thus q is_simple_vertex_seq_at h,j,n by A4,A5,A6,A12,A15,A27,A28,A52,A137,A142
,A145,Lm18;
A150: len pk > 1 by A27;
A151: pk is_vertex_seq_at g,Ak,n by A27;
A152: q.len pk=pk.len pk by A150,Lm1
.= Ak by A151;
hereby
let i;
assume that
A153: 1<=i and A154: i<len q ;
i < len pk +1 by A154,FINSEQ_2:16;
then A155: i <= len pk by NAT_1:13;
now per cases;
suppose i=len pk;
hence q.i in {Ak} or q.i in Ug by A152,TARSKI:def 1;
end;
suppose i<>len pk;
then A156: i < len pk by A155,XXREAL_0:1;
q.i=pk.i by A153,A155,Lm1;
hence q.i in {Ak} or q.i in Ug by A28,A153,A156;
end;
end;
hence q.i in Uh by A23,XBOOLE_0:def 3;
end;
A157: len Q =len PK+1 by A147,A149,FINSEQ_1:22;
A158: len pk=len PK+1 by A29;
then A159: len q=len Q + 1 by A157,FINSEQ_2:16;
set FS=the Source of G, FT=the Target of G;
now
let i be Nat;
assume that
A160: 1<=i and A161: i<=len Q ;
per cases;
suppose
A162: i=len Q;
then A163: Q.i=e by A147,A148,A149,A157,Lm2;
then A164: FT.(Q.i) = v3 by A146,GRAPH_4:def 1;
thus FS.(Q.i)=q.i by A146,A152,A157,A158,A162,A163,GRAPH_4:def 1;
thus FT.(Q.i) = q.(i+1) by A54,A157,A158,A162,A164,FINSEQ_1:42;
end;
suppose i<>len Q;
then A165: i < len Q by A161,XXREAL_0:1;
then A166: i <= len PK by A157,NAT_1:13;
then A167: FS.(PK.i) = pk.i by A29,A160;
A168: FT.(PK.i) = pk.(i+1) by A29,A160,A166;
A169: Q.i=PK.i by A149,A160,A166,Lm1;
A170: i+1 <= len pk by A157,A158,A165,NAT_1:13;
thus FS.(Q.i) = q.i by A157,A158,A160,A161,A167,A169,Lm1;
thus FT.(Q.i)=q.(i+1) by A168,A169,A170,Lm1,NAT_1:12;
end;
end;
hence Q is_oriented_edge_seq_of q by A159;
A171: cost(PK,W)+cost(pe,W)=cost(Q,W) by A17,A149,GRAPH_5:46,54;
A172: cost(pe,W) = W.(pe.1) by A17,A147,Th4,GRAPH_5:46
.=Weight(vk,v3,W) by A146,Th25;
then A173: newpathcost(M.g,n,j)=cost(Q,W) by A17,A42,A43,A83,A149,
GRAPH_5:46,54;
hereby
per cases;
suppose
A174: g.nj=-1;
now
let v2;
assume
A175: v2 in Ug;
then reconsider m=v2 as Element of NAT;
-1= f.(2*n+n*m+j) by A9,A57,A58,A174,A175
.=Weight(v2,v3,W) by A1,A54;
hence not ex e be set st e in the carrier' of G &
e orientedly_joins v2,v3 by Th23;
end;
hence Q is_shortestpath_of v1,v3,Uh,W
by A2,A7,A23,A30,A53,A146,A149,Th15;
end;
suppose
A176: g.nj <> -1;
then ex p,P st ( p is_simple_vertex_seq_at g,j,n)&( for i st 1<=
i & i<len p holds p.i in Ug)&( P is_oriented_edge_seq_of p)&( P
is_shortestpath_of v1,v3,Ug,W)&( cost(P,W)=g.m2)&( not v3 in Ug implies P
islongestInShortestpath Ug,v1,W) by A8,A53,A54;
hence Q is_shortestpath_of v1,v3,Uh,W by A2,A7,A13,A17,A21,A23,A30
,A32,A40,A42,A43,A53,A61,A64,A83,A84,A138,A146,A149,A171,A172,A176,Th18,
GRAPH_5:65;
end;
end;
thus cost(Q,W)=h.m2 by A15,A63,A65,A66,A67,A71,A136,A173,Def14;
0 <= cost(pe,W) by A17,GRAPH_5:50;
then A177: cost(PK,W)+0 <= cost(Q,W) by A171,XREAL_1:7;
hereby
assume not v3 in Uh;
now
let v2;
assume that
A178: v2 in Uh and A179: v2 <> v1 ;
per cases by A23,A178,XBOOLE_0:def 3;
suppose v2 in {Ak};
then A180: v2 = Ak by TARSKI:def 1;
take PK;
thus PK is_shortestpath_of v1,v2,Uh,W by A23,A30,A180,Th8;
thus cost(PK,W) <= cost(Q,W) by A177;
end;
suppose
A181: v2 in Ug;
then consider P such that
A182: P is_shortestpath_of v1,v2,Ug,W and A183: cost(P,W) <= cost(PK,W)
by A4,A5,A6,A32,A179,Th39,GRAPH_5:def 19;
A184: now
let R,v4;
assume that
A185: not v4 in Ug and A186: R is_shortestpath_of v1,v4,Ug,W ;
A187: v4 in VG;
then reconsider j4=v4 as Element of NAT;
A188: 1<=j4 by A16,A187,FINSEQ_1:1;
j4<=n by A16,A187,FINSEQ_1:1;
then
g.(n+j4) <> -1 by A1,A2,A7,A9,A17,A185,A186,A188,Lm19;
then consider rn being FinSequence of NAT,RR
be oriented Chain of G such that
rn is_simple_vertex_seq_at g,j4,n
and for i st 1<=i & i<len rn holds rn.i in Ug
and RR is_oriented_edge_seq_of rn
and A189: RR is_shortestpath_of v1,v4,Ug,W
and cost(RR,W) =g.(2*n+j4)
and A190: not v4 in Ug implies RR islongestInShortestpath Ug,v1,W
by A2,A7,A8,A185;
consider PP being oriented Chain of G such that
A191: PP is_shortestpath_of v1,v2,Ug,W
and A192: cost(PP,W) <= cost(RR,W) by A179,A181,A185,A190,GRAPH_5:def 19;
cost(PP,W)= cost(P,W) by A182,A191,Th9;
hence cost(P,W) <= cost(R,W) by A186,A189,A192,Th9;
end;
take P;
thus P is_shortestpath_of v1,v2,Uh,W
by A17,A24,A179,A182,A184,GRAPH_5:64;
thus cost(P,W) <= cost(Q,W) by A177,A183,XXREAL_0:2;
end;
end;
hence Q islongestInShortestpath Uh,v1,W by GRAPH_5:def 19;
end;
end;
end;
hereby
let m,j;
assume that
A193: h.(n+j) = -1 and A194: 1<=j
and A195: j<=n
and A196: m in Uh ;
set nj=n+j;
A197: 1 < nj by A194,A195,Lm12;
A198: nj <= 2*n by A194,A195,Lm12;
A199: nj < mi by A194,A195,Lm12;
then A200: nj in dom g by A12,A19,A197,FINSEQ_3:25;
n+1 <= nj by A194,XREAL_1:7;
then A201: n < nj by NAT_1:13;
A202: M.g hasBetterPathAt n,nj-'n implies
contradiction by A193,A14,A15,A42,A198,A200,A201,Def14;
A203: M.g.nj=g.nj by A13,A21,A199,A201,Th18;
then A204: g.nj=-1 by A14,A15,A193,A198,A200,A201,A202,Def14;
then A205: not j in Ug by A10;
j < mi by A25,A195,XXREAL_0:2;
then j in dom g by A12,A19,A194,FINSEQ_3:25;
then g.j<>-1 by A194,A195,A205;
then
A206: M.g.j <> -1 by A13,A22,A25,A195,A204,Th18;
not M.g hasBetterPathAt n,j by A202,NAT_D:34;
then A207: M.g/.(2*n+n*(M.g/.mi)+j) < 0 by A203,A204,A206;
reconsider v3=j as Vertex of G by A16,A194,A195,FINSEQ_1:1;
set Akj=2*n+n*Ak+j;
A208: 1 < Akj by A20,A21,A195,Lm13;
A209: Ak < Akj by A20,A21,A195,Lm13;
A210: Akj < mi by A20,A21,A195,Lm13;
then A211: Akj in dom g by A12,A19,A208,FINSEQ_3:25;
A212: 3*n+1 <=Akj by A20,A21,A194,A195,Lm14;
A213: Akj <= n*n+3*n by A20,A21,A194,A195,Lm14;
A214: f.Akj=Weight(vk,v3,W) by A1;
A215: M.g/.(2*n+n*(M.g/.mi)+j)=M.g.Akj by A14,A42,A211,PARTFUN1:def 6
.=g.Akj by A13,A209,A210,Th18
.=Weight(vk,v3,W) by A38,A211,A212,A213,A214;
per cases by A23,A196,XBOOLE_0:def 3;
suppose m in {Ak};
then A216: m=Ak by TARSKI:def 1;
not ex e be set st e in the carrier' of G & e orientedly_joins vk, v3
by A207,A215,Th23;
then Weight(vk,v3,W)=-1 by Def7;
hence f.(2*n+n*m+j) = -1 by A1,A216;
end;
suppose m in Ug;
hence f.(2*n+n*m+j) = -1 by A9,A194,A195,A204;
end;
end;
let m;
assume
A217: m in Uh;
per cases by A23,A217,XBOOLE_0:def 3;
suppose
A218: m in Ug;
then h.(n+m)=g.(n+m) by A4,A5,A6,A12,Lm16;
hence thesis by A10,A218;
end;
suppose m in {Ak};
hence thesis by A22,A52,TARSKI:def 1;
end;
end;
theorem
f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & 1 <> v2 & v2=i & n >= 1 & g=
(DijkstraAlgorithm(n)).f implies the carrier of G = UsedVx(g,n) \/ UnusedVx(g,n
) & (v2 in UsedVx(g,n) implies ex p,P st p is_simple_vertex_seq_at g,i,n & P
is_oriented_edge_seq_of p & P is_shortestpath_of v1,v2,W & cost(P,W)=g.(2*n+i))
& (v2 in UnusedVx(g,n) implies not ex Q st Q is_orientedpath_of v1,v2)
proof
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: v1=1 and
A3: 1 <> v2 and
A4: v2=i and
A5: n >= 1 and
A6: g=(DijkstraAlgorithm(n)).f;
A7: Seg n=the carrier of G by A1;
then reconsider VG=the carrier of G as non empty Subset of NAT by A5;
A8: f.(n+1) =0 by A1;
set Ug=UsedVx(g,n), Vg=UnusedVx(g,n);
set R=Relax(n), M=findmin(n), RM=repeat (R*M), cn=LifeSpan(R*M,f,n), mi=n*n+
3*n+1;
A9: g = RM.cn.f by A6,Def5;
A10: Ug \/ Vg c= VG
proof
let x be object;
assume
A11: x in Ug \/ Vg;
per cases by A11,XBOOLE_0:def 3;
suppose
x in Ug;
then ex k st x = k & k in dom g & 1 <= k & k <= n & g.k = -1;
hence thesis by A7,FINSEQ_1:1;
end;
suppose
x in Vg;
then ex k st x = k & k in dom g & 1 <= k & k <= n & g.k <> -1;
hence thesis by A7,FINSEQ_1:1;
end;
end;
A12: len f=mi by A1;
VG c= Ug \/ Vg
proof
let x be object;
assume
A13: x in VG;
then reconsider j=x as Element of NAT;
A14: 1 <= j by A7,A13,FINSEQ_1:1;
A15: j <= n by A7,A13,FINSEQ_1:1;
n < mi by Lm7;
then j < mi by A15,XXREAL_0:2;
then j in dom f by A12,A14,FINSEQ_3:25;
then
A16: j in dom g by A9,Th41;
per cases;
suppose
g.j=-1;
then j in {k: k in dom g & 1 <= k & k <= n & g.k = -1} by A14,A15,A16;
hence thesis by XBOOLE_0:def 3;
end;
suppose
g.j<>-1;
then
j in {k: k in dom g & 1 <= k & k <= n & g.k <> -1} by A14,A15,A16;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence
A17: the carrier of G = Ug \/ Vg by A10,XBOOLE_0:def 10;
defpred P[Nat] means
$1 <= cn implies (for v3,j st v3<>v1 & v3=j
& RM.$1.f.(n+j)<>-1 holds ex p,P st p is_simple_vertex_seq_at RM.$1.f,j,n & (
for m st 1<=m & m<len p holds p.m in UsedVx(RM.$1.f,n)) & P
is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3,UsedVx(RM.$1.f,n),W &
cost(P,W)=RM.$1.f.(2*n+j) & (not v3 in UsedVx(RM.$1.f,n) implies P
islongestInShortestpath UsedVx(RM.$1.f,n),v1,W )) & (for m,j st RM.$1.f.(n+j) =
-1 & 1<=j & j<=n & m in UsedVx(RM.$1.f,n) holds f.(2*n+n*m+j) = -1) & (for m st
m in UsedVx(RM.$1.f,n) holds RM.$1.f.(n+m) <> -1);
1 <= mi by NAT_1:12;
then
A18: 1 in dom f by A12,FINSEQ_3:25;
A19: ( for m st 1<=m & m<=n holds f.m=1)& for m st 2<=m & m<=n holds f.(n+m)
=-1 by A1;
then {1} = UsedVx(RM.1.f,n) by A5,A8,A18,Th47;
then
A20: 1 in UsedVx(RM.1.f,n) by TARSKI:def 1;
A21: for k st P[k] holds P[k+1]
proof
let k;
assume
A22: P[k];
now
set FK1=RM.(k+1).f, UV1=UsedVx(FK1,n);
set FK=RM.k.f;
assume
A23: k+1 <= cn;
then
A24: k < cn by NAT_1:13;
then
A25: OuterVx(FK,n) <> {} by Def4;
per cases;
suppose
k=0;
hence (for v3,j st v3<>v1 & v3=j & FK1.(n+j)<>-1 holds ex p,P st p
is_simple_vertex_seq_at FK1,j,n & (for m st 1<=m & m<len p holds p.m in UV1) &
P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3,UV1,W & cost(P,W)=FK1.
(2*n+j) & (not v3 in UV1 implies P islongestInShortestpath UV1,v1,W )) & (for m
,j st FK1.(n+j) = -1 & 1<=j & j<=n & m in UV1 holds f.(2*n+n*m+j) = -1) & for m
st m in UV1 holds FK1.(n+m) <> -1 by A1,A2,A5,Lm15;
end;
suppose
k<>0;
then k >= 1+0 by INT_1:7;
then 1 in UsedVx(FK,n) by A20,A24,Th48;
hence (for v3,j st v3<>v1 & v3=j & FK1.(n+j)<>-1 holds ex p,P st p
is_simple_vertex_seq_at FK1,j,n & (for m st 1<=m & m<len p holds p.m in UV1) &
P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3,UV1,W & cost(P,W)=FK1.
(2*n+j) & (not v3 in UV1 implies P islongestInShortestpath UV1,v1,W )) & (for m
,j st FK1.(n+j) = -1 & 1<=j & j<=n & m in UV1 holds f.(2*n+n*m+j) = -1) & for m
st m in UV1 holds FK1.(n+m) <> -1 by A1,A2,A5,A22,A23,A25,Lm20,NAT_1:13;
end;
end;
hence thesis;
end;
A26: RM.0 .f = f by Th21;
A27: P[0]
proof
set UV=UsedVx(RM.0 .f,n), h=RM.0 .f;
assume 0 <= cn;
hereby
let v3,j;
assume that
A28: v3<>v1 and
A29: v3=j and
A30: h.(n+j)<>-1;
A31: v3 in VG;
then 1<=j by A7,A29,FINSEQ_1:1;
then 1 < j by A2,A28,A29,XXREAL_0:1;
then
A32: 1+1 <= j by INT_1:7;
assume
not (ex p,P st p is_simple_vertex_seq_at h,j,n & (for m st 1<=m & m<
len p holds p.m in UV) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,
v3,UV,W & cost(P,W)=h.(2*n+j) & (not v3 in UV implies P islongestInShortestpath
UV,v1,W));
j<=n by A7,A29,A31,FINSEQ_1:1;
hence contradiction by A1,A26,A30,A32;
end;
thus for m,j st h.(n+j) = -1 & 1<=j & j<=n & m in UV & not f.(2*n+n*m+j) =
-1 holds contradiction by A5,A26,A8,A19,A18,Th47;
let m;
assume
A33: m in UsedVx(h,n);
assume h.(n+m) = -1;
thus contradiction by A5,A26,A8,A19,A18,A33,Th47;
end;
A34: for k holds P[k] from NAT_1:sch 2(A27,A21);
ex ii being Nat st ii<=n & OuterVx(RM.ii.f,n) = {} by Th40;
then
A35: OuterVx(g,n) = {} by A9,Def4;
A36: now
let v3,v4;
assume that
A37: v3 in Ug and
A38: v4 in Vg;
v3 in VG;
then reconsider m=v3 as Element of NAT;
consider j such that
A39: v4 = j and
A40: j in dom g and
A41: 1 <= j & j <= n and
A42: g.j <> -1 by A38;
now
assume g.(n+j) <> -1;
then j in {k: k in dom g & 1 <= k & k <= n & g.k <> -1 & g.(n+k) <> -1}
by A40,A41,A42;
hence contradiction by A35;
end;
then -1=f.(2*n+n*m+j) by A9,A34,A37,A41
.=Weight(v3,v4,W) by A1,A39;
hence not ex e st e in the carrier' of G & e orientedly_joins v3,v4 by Th23
;
end;
A43: f.1=1 by A1,A5;
now
assume
A44: cn=0;
1 in {k: k in dom f & 1 <= k & k <= n & f.k <> -1 & f.(n+k) <> -1} by A5
,A43,A8,A18;
hence contradiction by A9,A26,A35,A44;
end;
then cn >= 1+0 by INT_1:7;
then
A45: v1 in Ug by A2,A9,A20,Th48;
hereby
assume v2 in Ug;
then g.(n+i) <> -1 by A4,A9,A34;
then consider p,P such that
A46: p is_simple_vertex_seq_at g,i,n and
for m st 1<=m & m<len p holds p.m in Ug and
A47: P is_oriented_edge_seq_of p and
A48: P is_shortestpath_of v1,v2,Ug,W and
A49: cost(P,W)=g.(2*n+i) and
not v2 in Ug implies P islongestInShortestpath Ug,v1,W by A2,A3,A4,A9,A34;
take p,P;
thus p is_simple_vertex_seq_at g,i,n by A46;
thus P is_oriented_edge_seq_of p by A47;
thus P is_shortestpath_of v1,v2,W by A17,A36,A45,A48,Th16;
thus cost(P,W)=g.(2*n+i) by A49;
end;
thus thesis by A17,A36,A45,Th11;
end;