Every finite directed walk admits a no-longer simple path
ProvedEdmondsKarp.ShortestPath.chain_simplegraph-theorynetwork-flow
Every finite list forming a chain for a binary relation admits a list of distinct vertices forming a chain for the same relation, with identical first and last vertices and no greater length.
Preamble
import Mathlib
Formal statement
theorem EdmondsKarp.ShortestPath.chain_simple {V : Type} [DecidableEq V] (R : V → V → Prop) (P : List V)
(hP : P.IsChain R) :
∃ Q : List V, Q.Nodup ∧ Q.IsChain R ∧ Q.head? = P.head? ∧
Q.getLast? = P.getLast? ∧ Q.length ≤ P.length := by sorrySource
Auxiliary directed-path lemmas for Edmonds and Karp (1972), §1.1 p. 249 and §1.2 pp. 251–252. DOI: 10.1145/321694.321699.