let G be Graph; :: thesis: for p being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let p be oriented Chain of G; :: thesis: for W being Function
for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let W be Function; :: thesis: for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let V be set ; :: thesis: for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
let v1, v2 be Vertex of G; :: thesis: ( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
set V' = V \/ {v2};
hereby :: thesis: ( p is_shortestpath_of v1,v2,V \/ {v2},W implies p is_shortestpath_of v1,v2,V,W )
assume A1:
p is_shortestpath_of v1,
v2,
V,
W
;
:: thesis: p is_shortestpath_of v1,v2,V \/ {v2},Wthen
(
p is_orientedpath_of v1,
v2,
V & ( for
q being
oriented Chain of
G st
q is_orientedpath_of v1,
v2,
V holds
cost p,
W <= cost q,
W ) )
by GRAPH_5:def 18;
then A2:
p is_orientedpath_of v1,
v2,
V \/ {v2}
by Th7;
now let q be
oriented Chain of
G;
:: thesis: ( q is_orientedpath_of v1,v2,V \/ {v2} implies cost p,W <= cost q,W )assume
q is_orientedpath_of v1,
v2,
V \/ {v2}
;
:: thesis: cost p,W <= cost q,Wthen
q is_orientedpath_of v1,
v2,
V
by Th7;
hence
cost p,
W <= cost q,
W
by A1, GRAPH_5:def 18;
:: thesis: verum end; hence
p is_shortestpath_of v1,
v2,
V \/ {v2},
W
by A2, GRAPH_5:def 18;
:: thesis: verum
end;
assume A3:
p is_shortestpath_of v1,v2,V \/ {v2},W
; :: thesis: p is_shortestpath_of v1,v2,V,W
then
( p is_orientedpath_of v1,v2,V \/ {v2} & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V \/ {v2} holds
cost p,W <= cost q,W ) )
by GRAPH_5:def 18;
then A4:
p is_orientedpath_of v1,v2,V
by Th7;
now let q be
oriented Chain of
G;
:: thesis: ( q is_orientedpath_of v1,v2,V implies cost p,W <= cost q,W )assume
q is_orientedpath_of v1,
v2,
V
;
:: thesis: cost p,W <= cost q,Wthen
q is_orientedpath_of v1,
v2,
V \/ {v2}
by Th7;
hence
cost p,
W <= cost q,
W
by A3, GRAPH_5:def 18;
:: thesis: verum end;
hence
p is_shortestpath_of v1,v2,V,W
by A4, GRAPH_5:def 18; :: thesis: verum