:: deftheorem Def14 defines AP:GetAugPath GLIB_005:def 14 :
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being Vertex of G
for b₅ being vertex-distinct Path of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) implies ( b₅ = AP:GetAugPath (EL,source,sink) iff ( b₅ is_Walk_from source,sink & b₅ is_augmenting_wrt EL & ( for n being even Nat st n in dom b₅ holds
b₅ . n = (AP:FindAugPath (EL,source)) . (b₅ . (n + 1)) ) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ( b₅ = AP:GetAugPath (EL,source,sink) iff b₅ = G .walkOf source ) ) );