:: deftheorem defines is_augmenting_wrt GLIB_005:def 8 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G holds
( W is_augmenting_wrt EL iff for n being odd Nat st n < len W holds
( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) ) );