:: deftheorem Def17 defines FF:PushFlow GLIB_005:def 17 :
for G being natural-weighted WGraph
for EL being FF:ELabeling of G
for P being Path of G st P is_augmenting_wrt EL holds
for b₄ being FF:ELabeling of G holds
( b₄ = FF:PushFlow (EL,P) iff ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b₄ . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b₄ . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b₄ . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) ) );