let G be Graph; 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; 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; 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 ; 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; ( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
set V9 = V \/ {v2};
hereby ( 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
;
p is_shortestpath_of v1,v2,V \/ {v2},WA2:
now for q being oriented Chain of G st q is_orientedpath_of v1,v2,V \/ {v2} holds
cost (p,W) <= cost (q,W)let q be
oriented Chain of
G;
( q is_orientedpath_of v1,v2,V \/ {v2} implies cost (p,W) <= cost (q,W) )assume
q is_orientedpath_of v1,
v2,
V \/ {v2}
;
cost (p,W) <= cost (q,W)then
q is_orientedpath_of v1,
v2,
V
by Th7;
hence
cost (
p,
W)
<= cost (
q,
W)
by A1, GRAPH_5:def 18;
verum end;
p is_orientedpath_of v1,
v2,
V
by A1, GRAPH_5:def 18;
then
p is_orientedpath_of v1,
v2,
V \/ {v2}
by Th7;
hence
p is_shortestpath_of v1,
v2,
V \/ {v2},
W
by A2, GRAPH_5:def 18;
verum
end;
assume A3:
p is_shortestpath_of v1,v2,V \/ {v2},W
; p is_shortestpath_of v1,v2,V,W
A4:
now for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost (p,W) <= cost (q,W)let q be
oriented Chain of
G;
( q is_orientedpath_of v1,v2,V implies cost (p,W) <= cost (q,W) )assume
q is_orientedpath_of v1,
v2,
V
;
cost (p,W) <= cost (q,W)then
q is_orientedpath_of v1,
v2,
V \/ {v2}
by Th7;
hence
cost (
p,
W)
<= cost (
q,
W)
by A3, GRAPH_5:def 18;
verum end;
p is_orientedpath_of v1,v2,V \/ {v2}
by A3, GRAPH_5:def 18;
then
p is_orientedpath_of v1,v2,V
by Th7;
hence
p is_shortestpath_of v1,v2,V,W
by A4, GRAPH_5:def 18; verum