New residual arcs reverse a step of the augmenting path
ProvedEdmondsKarp.ShortestPath.augment_residual_subgraph-theorynetwork-flow
Every residual arc after augmentation either was residual before augmentation or is the reversal of a step on the augmenting path.
Preamble
import Definitions.Def_EdmondsKarp_ShortestPath_Augmentation open EdmondsKarp.ShortestPath
Formal statement
theorem EdmondsKarp.ShortestPath.augment_residual_sub {V : Type} [Fintype V] [DecidableEq V] (N : Network V)
(f : V → V → ℝ) (P : List V) (hf : IsFlow N f) (hP : IsAugPath N f P)
(u v : V) (h : ResArc N (augment N f P) u v) :
ResArc N f u v ∨ (v, u) ∈ pathArcs P := by sorrySource
Edmonds and Karp (1972), Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, §1.1 pp. 249–250 and §1.2 p. 251. DOI: 10.1145/321694.321699.