let G be real-weighted WGraph; for EL being FF:ELabeling of G
for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
let EL be FF:ELabeling of G; for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
let W be Walk of G; for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
let m, n be Nat; ( W is_augmenting_wrt EL implies W .cut (m,n) is_augmenting_wrt EL )
set W2 = W .cut (m,n);
assume A1:
W is_augmenting_wrt EL
; W .cut (m,n) is_augmenting_wrt EL
now W .cut (m,n) is_augmenting_wrt ELper 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 A2:
(
m is
odd &
n is
odd &
m <= n &
n <= len W )
;
W .cut (m,n) is_augmenting_wrt ELthen reconsider m9 =
m,
n9 =
n as
odd Element of
NAT by ORDINAL1:def 12;
now for x being odd Nat st x < len (W .cut (m,n)) holds
( ( (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) ) & ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) ) )let x be
odd Nat;
( x < len (W .cut (m,n)) implies ( ( (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) ) & ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) ) ) )reconsider x9 =
x as
Element of
NAT by ORDINAL1:def 12;
set v1b =
(W .cut (m,n)) . x;
set eb =
(W .cut (m,n)) . (x + 1);
set v2b =
(W .cut (m,n)) . (x + 2);
assume A3:
x < len (W .cut (m,n))
;
( ( (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1)) ) & ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) ) )then A4:
x9 in dom (W .cut (m,n))
by GLIB_001:12;
A5:
m9 <= n9
by A2;
A6:
x9 + 2
in dom (W .cut (m,n))
by A3, GLIB_001:12;
then A7:
(W .cut (m,n)) . (x9 + 2) = W . ((m9 + (x9 + 2)) - 1)
by A2, A5, GLIB_001:47;
x9 + 1
in dom (W .cut (m,n))
by A3, GLIB_001:12;
then A8:
(W .cut (m,n)) . (x9 + 1) = W . ((m9 + (x9 + 1)) - 1)
by A2, A5, GLIB_001:47;
(m9 + x9) - 1
in dom W
by A2, A4, A5, GLIB_001:47;
then reconsider a =
(m9 + x) - 1,
a2 =
(m + (x + 2)) - 1 as
Element of
NAT by A8;
reconsider a =
a as
odd Element of
NAT ;
set v1a =
W . a;
set ea =
W . (a + 1);
set v2a =
W . (a + 2);
(m9 + (x9 + 2)) - 1
in dom W
by A2, A6, A5, GLIB_001:47;
then
a2 <= len W
by FINSEQ_3:25;
then A9:
((m + (x + 2)) - 1) - 2
< (len W) - 0
by XREAL_1:15;
hereby ( not (W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,(W .cut (m,n)) . (x + 2),G implies 0 < EL . ((W .cut (m,n)) . (x + 1)) )
assume
(W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,
(W .cut (m,n)) . (x + 2),
G
;
EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1))then
W . (a + 1) DJoins W . a,
W . (a + 2),
G
by A2, A4, A5, A8, A7, GLIB_001:47;
hence
EL . ((W .cut (m,n)) . (x + 1)) < (the_Weight_of G) . ((W .cut (m,n)) . (x + 1))
by A1, A8, A9;
verum
end; assume
not
(W .cut (m,n)) . (x + 1) DJoins (W .cut (m,n)) . x,
(W .cut (m,n)) . (x + 2),
G
;
0 < EL . ((W .cut (m,n)) . (x + 1))then
not
W . (a + 1) DJoins W . a,
W . (a + 2),
G
by A2, A4, A5, A8, A7, GLIB_001:47;
hence
0 < EL . ((W .cut (m,n)) . (x + 1))
by A1, A8, A9;
verum end; hence
W .cut (
m,
n)
is_augmenting_wrt EL
;
verum end;
hence
W .cut (m,n) is_augmenting_wrt EL
; verum