let G be _finite nonnegative-weighted WGraph; for W being DPath of G
for x, y being set
for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
let W be DPath of G; for x, y being set
for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
let x, y be set ; for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
let m, n be Element of NAT ; ( W is_mincost_DPath_from x,y implies W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() )
set WC = W .cut (m,n);
A1:
W .cut (m,n) is_Walk_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
by GLIB_001:def 23;
assume A2:
W is_mincost_DPath_from x,y
; W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
then A3:
W is_Walk_from x,y
;
then A4:
( W . 1 = x & W . (len W) = y )
by GLIB_001:17;
now W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() per cases
( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W )
;
suppose A5:
(
m is
odd &
n is
odd &
m <= n &
n <= len W )
;
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() set W1 =
W .cut (1,
m);
set W3 =
W .cut (
n,
(len W));
A6:
1
<= n
by A5, ABIAN:12;
then A7:
(W .cut (1,n)) .append (W .cut (n,(len W))) =
W .cut (1,
(len W))
by A5, GLIB_001:38, JORDAN12:2
.=
W
by GLIB_001:39
;
(W .cut (1,n)) .last() =
W . n
by A5, A6, GLIB_001:37, JORDAN12:2
.=
(W .cut (n,(len W))) .first()
by A5, GLIB_001:37
;
then A8:
W .cost() = ((W .cut (1,n)) .cost()) + ((W .cut (n,(len W))) .cost())
by A7, GLIB_003:24;
A9:
1
<= m
by A5, ABIAN:12;
then A10:
(W .cut (1,m)) .append (W .cut (m,n)) = W .cut (1,
n)
by A5, GLIB_001:38, JORDAN12:2;
A11:
m <= len W
by A5, XXREAL_0:2;
then (W .cut (1,m)) .last() =
W . m
by A5, A9, GLIB_001:37, JORDAN12:2
.=
(W .cut (m,n)) .first()
by A5, GLIB_001:37
;
then
(W .cut (1,n)) .cost() = ((W .cut (1,m)) .cost()) + ((W .cut (m,n)) .cost())
by A10, GLIB_003:24;
then A12:
W .cost() = ((W .cut (m,n)) .cost()) + (((W .cut (1,m)) .cost()) + ((W .cut (n,(len W))) .cost()))
by A8;
A13:
W .cut (
n,
(len W))
is_Walk_from W . n,
W . (len W)
by A5, GLIB_001:37;
A14:
W .cut (1,
m)
is_Walk_from W . 1,
W . m
by A5, A9, A11, GLIB_001:37, JORDAN12:2;
now W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() assume
not
W .cut (
m,
n)
is_mincost_DPath_from (W .cut (m,n)) .first() ,
(W .cut (m,n)) .last()
;
contradictionthen consider W2 being
DPath of
G such that A15:
W2 is_Walk_from (W .cut (m,n)) .first() ,
(W .cut (m,n)) .last()
and A16:
W2 .cost() < (W .cut (m,n)) .cost()
by A1;
set WA =
(W .cut (1,m)) .append W2;
set WB =
((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)));
set WB2 = the
DPath of
((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)));
A17:
(W .cut (m,n)) .last() = W . n
by A5, GLIB_001:37;
A18:
(W .cut (m,n)) .first() = W . m
by A5, GLIB_001:37;
then
(W .cut (1,m)) .append W2 is_Walk_from W . 1,
W . n
by A14, A15, A17, GLIB_001:31;
then
((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) is_Walk_from x,
y
by A4, A13, GLIB_001:31;
then A19:
the
DPath of
((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) is_Walk_from x,
y
by GLIB_001:160;
W2 .first() = W . m
by A15, A18, GLIB_001:def 23;
then A20:
(W .cut (1,m)) .last() = W2 .first()
by A5, A9, A11, GLIB_001:37, JORDAN12:2;
then A21:
((W .cut (1,m)) .append W2) .cost() = ((W .cut (1,m)) .cost()) + (W2 .cost())
by GLIB_003:24;
W2 .last() = W . n
by A15, A17, GLIB_001:def 23;
then (W .cut (n,(len W))) .first() =
W2 .last()
by A5, GLIB_001:37
.=
((W .cut (1,m)) .append W2) .last()
by A20, GLIB_001:30
;
then (((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)))) .cost() =
(((W .cut (1,m)) .cost()) + (W2 .cost())) + ((W .cut (n,(len W))) .cost())
by A21, GLIB_003:24
.=
(W2 .cost()) + (((W .cut (1,m)) .cost()) + ((W .cut (n,(len W))) .cost()))
;
then A22:
(((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)))) .cost() < W .cost()
by A12, A16, XREAL_1:8;
the
DPath of
((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) .cost() <= (((W .cut (1,m)) .append W2) .append (W .cut (n,(len W)))) .cost()
by GLIB_003:30;
then
the
DPath of
((W .cut (1,m)) .append W2) .append (W .cut (n,(len W))) .cost() < W .cost()
by A22, XXREAL_0:2;
hence
contradiction
by A2, A19;
verum end; hence
W .cut (
m,
n)
is_mincost_DPath_from (W .cut (m,n)) .first() ,
(W .cut (m,n)) .last()
;
verum end;
hence
W .cut (m,n) is_mincost_DPath_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last()
; verum