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

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

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

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

theorem NetworkFlow.resCap'_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) : 0 ≤ resCap' N fl u v

theorem NetworkFlow.ResReachable_step {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} {fl : STFlow N} {u v : V} (hu : ResReachable N fl u) (hadj : resAdj' N fl u v) : ResReachable N fl v

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

theorem NetworkFlow.mem_resReachableSet_iff {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (v : V) : v ∈ resReachableSet N fl ↔ ResReachable N fl v

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

theorem NetworkFlow.t_not_mem_resReachableSet {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hmax : NoAugmentingPath N fl) : N.t ∉ resReachableSet N fl

noncomputable def NetworkFlow.maxFlowCut {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hmax : NoAugmentingPath N fl) : STCut N

theorem NetworkFlow.maxFlowCut_S {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hmax : NoAugmentingPath N fl) : (maxFlowCut N fl hmax).S = resReachableSet N fl

theorem NetworkFlow.not_resAdj_of_reach_nonreach {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} {fl : STFlow N} {u v : V} (hu : ResReachable N fl u) (hv : ¬ResReachable N fl v) : ¬resAdj' N fl u v

theorem NetworkFlow.resCap'_eq_zero_of_cross {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} {fl : STFlow N} {u v : V} (hu : ResReachable N fl u) (hv : ¬ResReachable N fl v) : resCap' N fl u v = 0

theorem NetworkFlow.flow_eq_cap_of_cross {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} {fl : STFlow N} {u v : V} (hu : ResReachable N fl u) (hv : ¬ResReachable N fl v) : fl.f u v = N.cap u v

theorem NetworkFlow.flow_eq_zero_of_cross {V : Type u_1} [Fintype V] [DecidableEq V] {N : FlowNetwork V} {fl : STFlow N} {u v : V} (hu : ResReachable N fl u) (hv : ¬ResReachable N fl v) : fl.f v u = 0

theorem NetworkFlow.flowValue_eq_cross {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (C : STCut N) : flowValue N fl = ∑ u ∈ C.S, ∑ v ∈ C.Sᶜ, fl.f u v - ∑ u ∈ C.S, ∑ v ∈ C.Sᶜ, fl.f v u

theorem NetworkFlow.max_flow_min_cut {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hmax : NoAugmentingPath N fl) : ∃ (C : STCut N), flowValue N fl = cutCapacity N C