structure NetworkFlow.DirectedGraph (V : Type u_2) [Fintype V] [DecidableEq V] : Type u_2

• edge : V → V → Prop
• edge_decidable (u v : V) : Decidable (self.edge u v)
• s : V
• t : V
• s_ne_t : self.s ≠ self.t

@[implicit_reducible]

instance NetworkFlow.instDecidableEdge {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (u v : V) : Decidable (G.edge u v)

structure NetworkFlow.DirPath {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : Type u_1

• vertices : List V
• nonempty : self.vertices ≠ []
• starts_at_s : self.vertices.head ⋯ = G.s
• ends_at_t : self.vertices.getLast ⋯ = G.t
• length_ge_two : self.vertices.length ≥ 2
• nodup : self.vertices.Nodup
• edges_valid (e : V × V) : e ∈ self.vertices.zip self.vertices.tail → G.edge e.1 e.2

def NetworkFlow.DirPath.edges {V : Type u_1} [Fintype V] [DecidableEq V] {G : DirectedGraph V} (p : DirPath G) : List (V × V)

def NetworkFlow.PairwiseEdgeDisjoint {V : Type u_1} [Fintype V] [DecidableEq V] {k : ℕ} {G : DirectedGraph V} (paths : Fin k → DirPath G) : Prop

structure NetworkFlow.EdgeDisjointPaths {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (k : ℕ) : Type u_1

• paths : Fin k → DirPath G
• disjoint : PairwiseEdgeDisjoint self.paths

noncomputable def NetworkFlow.minSTCutSize {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : ℕ

noncomputable def NetworkFlow.maxEdgeDisjointPaths {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : ℕ

def NetworkFlow.DirectedGraph.toFlowNetwork {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : FlowNetwork V

theorem NetworkFlow.list_crossing {α : Type u_2} (P : α → Prop) [DecidablePred P] (l : List α) (hl : l ≠ []) : P (l.head hl) → ¬P (l.getLast hl) → ∃ e ∈ l.zip l.tail, P e.1 ∧ ¬P e.2

theorem NetworkFlow.path_crosses_cut {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (p : DirPath G) (S : Finset V) (hs : G.s ∈ S) (ht : G.t ∉ S) : ∃ e ∈ p.edges, e.1 ∈ S ∧ e.2 ∈ Sᶜ ∧ G.edge e.1 e.2

theorem NetworkFlow.edgeDisjointPaths_le_cutSize {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (k : ℕ) (edp : EdgeDisjointPaths G k) (S : Finset V) (hs : G.s ∈ S) (ht : G.t ∉ S) : k ≤ {p : V × V | p.1 ∈ S ∧ p.2 ∈ Sᶜ ∧ G.edge p.1 p.2}.card

theorem NetworkFlow.maxEdgeDisjointPaths_le_minSTCutSize {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : maxEdgeDisjointPaths G ≤ minSTCutSize G

def NetworkFlow.DirectedGraph.removePathEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (p : DirPath G) : DirectedGraph V

theorem NetworkFlow.exists_maxFlow {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) : ∃ (fl : STFlow N), NoAugmentingPath N fl

theorem NetworkFlow.cutCapacity_eq_crossing_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (C : STCut G.toFlowNetwork) : cutCapacity G.toFlowNetwork C = ↑{p : V × V | p.1 ∈ C.S ∧ p.2 ∈ C.Sᶜ ∧ G.edge p.1 p.2}.card

theorem NetworkFlow.unit_cap_max_flow_integral {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (fl : STFlow G.toFlowNetwork) (hmax : NoAugmentingPath G.toFlowNetwork fl) (u v : V) : fl.f u v = 0 ∨ fl.f u v = 1

theorem NetworkFlow.integral_unit_flow_path_extraction {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (fl : STFlow G.toFlowNetwork) (hint : ∀ (u v : V), fl.f u v = 0 ∨ fl.f u v = 1) (k : ℕ) (hval : flowValue G.toFlowNetwork fl = ↑k) : Nonempty (EdgeDisjointPaths G k)

theorem NetworkFlow.ford_fulkerson_integrality_paths {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) (fl : STFlow G.toFlowNetwork) (hmax : NoAugmentingPath G.toFlowNetwork fl) (k : ℕ) (hval : flowValue G.toFlowNetwork fl = ↑k) : Nonempty (EdgeDisjointPaths G k)

theorem NetworkFlow.unit_flow_to_paths {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : ∃ (k : ℕ) (edp : EdgeDisjointPaths G k) (C : STCut G.toFlowNetwork), k = {p : V × V | p.1 ∈ C.S ∧ p.2 ∈ C.Sᶜ ∧ G.edge p.1 p.2}.card ∧ ∀ (C' : STCut G.toFlowNetwork), k ≤ {p : V × V | p.1 ∈ C'.S ∧ p.2 ∈ C'.Sᶜ ∧ G.edge p.1 p.2}.card

theorem NetworkFlow.minSTCutSize_le_maxEdgeDisjointPaths {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : minSTCutSize G ≤ maxEdgeDisjointPaths G

theorem NetworkFlow.menger {V : Type u_1} [Fintype V] [DecidableEq V] (G : DirectedGraph V) : maxEdgeDisjointPaths G = minSTCutSize G