let G be real-weighted WGraph; for EL being FF:ELabeling of G
for W being Walk of G
for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
let EL be FF:ELabeling of G; for W being Walk of G
for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
let W be Walk of G; for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
let e, v be set ; ( W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) implies W .addEdge e is_augmenting_wrt EL )
assume A1:
W is_augmenting_wrt EL
; ( v in W .vertices() or ( not ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) & not ( e DJoins v,W .last() ,G & 0 < EL . e ) ) or W .addEdge e is_augmenting_wrt EL )
set W2 = W .addEdge e;
assume that
A2:
not v in W .vertices()
and
A3:
( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) )
; W .addEdge e is_augmenting_wrt EL
let n be odd Nat; GLIB_005:def 8 ( n < len (W .addEdge e) implies ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) ) )
A4:
e Joins W .last() ,v,G
by A3;
assume A5:
n < len (W .addEdge e)
; ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )
now ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )per cases
( n < len W or n >= len W )
;
suppose A6:
n < len W
;
( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )reconsider n9 =
n as
Element of
NAT by ORDINAL1:def 12;
n9 + 1
in dom W
by A6, GLIB_001:12;
then A7:
W . (n + 1) = (W .addEdge e) . (n + 1)
by A4, GLIB_001:65;
n9 + 2
in dom W
by A6, GLIB_001:12;
then A8:
W . (n + 2) = (W .addEdge e) . (n + 2)
by A4, GLIB_001:65;
n9 in dom W
by A6, GLIB_001:12;
then
W . n = (W .addEdge e) . n
by A4, GLIB_001:65;
hence
( (
(W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,
(W .addEdge e) . (n + 2),
G implies
EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not
(W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,
(W .addEdge e) . (n + 2),
G implies
0 < EL . ((W .addEdge e) . (n + 1)) ) )
by A1, A6, A7, A8;
verum end; suppose A9:
n >= len W
;
( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )
n + 1
<= len (W .addEdge e)
by A5, NAT_1:13;
then
n + 1
<= (len W) + (2 * 1)
by A4, GLIB_001:64;
then
n + 1
< ((len W) + 1) + 1
by XXREAL_0:1;
then
n + 1
<= (len W) + 1
by NAT_1:13;
then A10:
n <= len W
by XREAL_1:6;
then A11:
n = len W
by A9, XXREAL_0:1;
then A12:
(W .addEdge e) . (n + 1) = e
by A4, GLIB_001:65;
1
<= n
by ABIAN:12;
then
n in dom W
by A10, FINSEQ_3:25;
then A13:
(W .addEdge e) . n =
W . n
by A4, GLIB_001:65
.=
W .last()
by A11, GLIB_001:def 7
;
( not
e DJoins W .last() ,
v,
G or not
e DJoins v,
W .last() ,
G )
by A2, GLIB_001:88;
hence
(
(W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,
(W .addEdge e) . (n + 2),
G implies
EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) )
by A3, A13, A12;
( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) )assume
not
(W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,
(W .addEdge e) . (n + 2),
G
;
0 < EL . ((W .addEdge e) . (n + 1))hence
0 < EL . ((W .addEdge e) . (n + 1))
by A3, A4, A11, A13, A12, GLIB_001:65;
verum end;
hence
( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )
; verum