noncomputable def NetworkFlow.flowSupport {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : Finset (V × V)

structure NetworkFlow.FlowPath {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) : Type u_1

• vertices : List V
• nonempty : self.vertices ≠ []
• starts_at_s : self.vertices.head ⋯ = N.s
• ends_at_t : self.vertices.getLast ⋯ = N.t
• length_ge_two : self.vertices.length ≥ 2
• nodup : self.vertices.Nodup

def NetworkFlow.FlowPath.edges {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} (p : FlowPath N) : List (V × V)

def NetworkFlow.FlowPath.mem_edges {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} (p : FlowPath N) (u v : V) : Prop

@[implicit_reducible]

instance NetworkFlow.FlowPath.decidable_mem_edges {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} (p : FlowPath N) (u v : V) : Decidable (p.mem_edges u v)

structure NetworkFlow.FlowDecomposition {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : Type u_1

• f' : STFlow N
• same_value : flowValue N self.f' = flowValue N fl
• support_sub : flowSupport N self.f' ⊆ flowSupport N fl
• k : ℕ
• paths : Fin self.k → FlowPath N
• weights : Fin self.k → ℝ
• weights_pos (i : Fin self.k) : 0 < self.weights i
• flow_eq (u v : V) : self.f'.f u v = ∑ i : Fin self.k, if (self.paths i).mem_edges u v then self.weights i else 0
• k_le_support : self.k ≤ (flowSupport N fl).card

theorem NetworkFlow.zero_of_flowSupport_empty {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hsupp : flowSupport N fl = ∅) (u v : V) : fl.f u v = 0

def NetworkFlow.reachableInSupport {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) : Prop

noncomputable def NetworkFlow.reachableSet {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : Finset V

theorem NetworkFlow.s_mem_reachableSet {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : N.s ∈ reachableSet N fl

theorem NetworkFlow.reachable_step {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) (hu : u ∈ reachableSet N fl) (hfuv : fl.f u v > 0) : v ∈ reachableSet N fl

theorem NetworkFlow.flow_zero_across_reachable {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) (hu : u ∈ reachableSet N fl) (hv : v ∉ reachableSet N fl) : fl.f u v = 0

theorem NetworkFlow.flowValue_nonpos_of_t_unreachable {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (ht : N.t ∉ reachableSet N fl) : flowValue N fl ≤ 0

theorem NetworkFlow.t_reachable_of_pos_value {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hpos : 0 < flowValue N fl) : N.t ∈ reachableSet N fl

theorem NetworkFlow.IsChain_zip_tail {α : Type u_2} (r : α → α → Prop) (l : List α) (hchain : List.IsChain r l) (e : α × α) : e ∈ l.zip l.tail → r e.1 e.2

theorem NetworkFlow.FlowPath.edges_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} (p : FlowPath N) : p.edges ≠ []

theorem NetworkFlow.exists_nodup_chain {V : Type u_1} [Fintype V] [DecidableEq V] (R : V → V → Prop) (a b : V) (hab : a ≠ b) (hreach : Relation.ReflTransGen R a b) : ∃ (l : List V) (hne : l ≠ []), List.IsChain R l ∧ l.Nodup ∧ l.head hne = a ∧ l.getLast hne = b ∧ l.length ≥ 2

theorem NetworkFlow.exists_flow_path_of_pos_value {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hval : 0 < flowValue N fl) : ∃ (p : FlowPath N), ∀ e ∈ p.edges, fl.f e.1 e.2 > 0

theorem NetworkFlow.remove_cycle_step {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hsupp : flowSupport N fl ≠ ∅) (hval : flowValue N fl = 0) : ∃ (fl' : STFlow N), flowValue N fl' = flowValue N fl ∧ flowSupport N fl' ⊂ flowSupport N fl

theorem NetworkFlow.decompose_one_step {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hval : 0 < flowValue N fl) : ∃ (p : FlowPath N) (w : ℝ) (fl' : STFlow N), 0 < w ∧ (∀ (u v : V), fl.f u v = fl'.f u v + if p.mem_edges u v then w else 0) ∧ flowSupport N fl' ⊂ flowSupport N fl

theorem NetworkFlow.remove_all_cycles {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : ∃ (fl' : STFlow N), flowValue N fl' = flowValue N fl ∧ flowSupport N fl' ⊆ flowSupport N fl ∧ ∀ (g : STFlow N), flowSupport N g ⊆ flowSupport N fl' → flowSupport N g ≠ ∅ → 0 < flowValue N g

theorem NetworkFlow.flow_decomposition_exists {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : Nonempty (FlowDecomposition N fl)