let G be _finite real-weighted WGraph; for src being Vertex of G
for n being Nat holds
( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )
let src be Vertex of G; for n being Nat holds
( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )
let n be Nat; ( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )
set DCS = DIJK:CompSeq src;
set RFS = G .reachableDFrom src;
set Gn = (DIJK:CompSeq src) . n;
set Gn1a = (DIJK:CompSeq src) . (n + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set SGn = the_Source_of G;
set TGn = the_Target_of G;
hereby ( dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src implies DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} )
assume A1:
DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {}
;
dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom srcnow not dom (((DIJK:CompSeq src) . n) `1) <> G .reachableDFrom srcdefpred S1[
set ]
means (
(the_Source_of G) . $1
in dom (((DIJK:CompSeq src) . n) `1) & not
(the_Target_of G) . $1
in dom (((DIJK:CompSeq src) . n) `1) );
assume A2:
dom (((DIJK:CompSeq src) . n) `1) <> G .reachableDFrom src
;
contradictionconsider BE1 being
Subset of
(the_Edges_of G) such that A3:
for
x being
set holds
(
x in BE1 iff (
x in the_Edges_of G &
S1[
x] ) )
from SUBSET_1:sch 1();
dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src
by Th19;
then A4:
dom (((DIJK:CompSeq src) . n) `1) c< G .reachableDFrom src
by A2, XBOOLE_0:def 8;
now not BE1 = {}
(DIJK:CompSeq src) . 0 = DIJK:Init src
by Def11;
then
dom (((DIJK:CompSeq src) . 0) `1) = {src}
;
then A5:
src in dom (((DIJK:CompSeq src) . 0) `1)
by TARSKI:def 1;
assume A6:
BE1 = {}
;
contradictionconsider v being
object such that A7:
v in G .reachableDFrom src
and A8:
not
v in dom (((DIJK:CompSeq src) . n) `1)
by A4, XBOOLE_0:6;
reconsider v =
v as
Vertex of
G by A7;
consider W being
directed Walk of
G such that A9:
W is_Walk_from src,
v
by A7, GLIB_002:def 6;
defpred S2[
Nat]
means ( $1 is
odd & $1
<= len W & not
W . $1
in dom (((DIJK:CompSeq src) . n) `1) );
W . (len W) =
W .last()
by GLIB_001:def 7
.=
v
by A9, GLIB_001:def 23
;
then A10:
ex
k being
Nat st
S2[
k]
by A8;
consider k being
Nat such that A11:
(
S2[
k] & ( for
m being
Nat st
S2[
m] holds
k <= m ) )
from NAT_1:sch 5(A10);
A12:
dom (((DIJK:CompSeq src) . 0) `1) c= dom (((DIJK:CompSeq src) . n) `1)
by Th18;
now contradictionper cases
( k = 1 or k <> 1 )
;
suppose A13:
k <> 1
;
contradictionreconsider k9 =
k as
odd Element of
NAT by A11, ORDINAL1:def 12;
1
<= k
by A11, ABIAN:12;
then
1
< k
by A13, XXREAL_0:1;
then
1
+ 1
< k + 1
by XREAL_1:8;
then
2
* 1
<= k
by NAT_1:13;
then reconsider k2a =
k9 - (2 * 1) as
odd Element of
NAT by INT_1:5;
set e =
W . (k2a + 1);
A14:
k - 2
< (len W) - 0
by A11, XREAL_1:15;
then A15:
W . (k2a + 1) DJoins W . k2a,
W . (k2a + 2),
G
by GLIB_001:122;
then A16:
(the_Target_of G) . (W . (k2a + 1)) = W . (k2a + 2)
;
k2a < k - 0
by XREAL_1:15;
then A17:
W . k2a in dom (((DIJK:CompSeq src) . n) `1)
by A11, A14;
(
W . (k2a + 1) in the_Edges_of G &
(the_Source_of G) . (W . (k2a + 1)) = W . k2a )
by A15;
hence
contradiction
by A3, A6, A11, A17, A16;
verum end; end; end; hence
contradiction
;
verum end; then reconsider BE1 =
BE1 as non
empty finite set ;
deffunc H1(
Element of
BE1)
-> set =
((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . $1)) + ((the_Weight_of G) . $1);
consider e1 being
Element of
BE1 such that A18:
for
e2 being
Element of
BE1 holds
H1(
e1)
<= H1(
e2)
from PRE_CIRC:sch 5();
A19:
not
(the_Target_of G) . e1 in dom (((DIJK:CompSeq src) . n) `1)
by A3;
A20:
e1 in the_Edges_of G
by A3;
then
(the_Target_of G) . e1 in the_Vertices_of G
by FUNCT_2:5;
then A21:
(the_Target_of G) . e1 in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1))
by A19, XBOOLE_0:def 5;
(the_Source_of G) . e1 in dom (((DIJK:CompSeq src) . n) `1)
by A3;
then
e1 DSJoins dom (((DIJK:CompSeq src) . n) `1),
(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),
G
by A20, A21;
hence
contradiction
by A1, A22, Def7;
verum end; hence
dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src
;
verum
end;
assume A25:
dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src
; DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {}
A26:
(DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n)
by Def11;
hence
DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {}
; verum