structure SimpleGraph.EdmondsExecution {V : Type u_1} (G : SimpleGraph V) : Type u_1

• numPhases : ℕ
• matching : Fin (self.numPhases + 1) → G.Subgraph
• isMatching (i : Fin (self.numPhases + 1)) : (self.matching i).IsMatching
• size_increases_by_one (i : Fin self.numPhases) : (self.matching ⟨↑i + 1, ⋯⟩).edgeSet.ncard = (self.matching ⟨↑i, ⋯⟩).edgeSet.ncard + 1
• isFinalMaximum : (self.matching ⟨self.numPhases, ⋯⟩).IsMaxMatching

structure SimpleGraph.EdmondsPhaseDetail {V : Type u_1} [Fintype V] (G : SimpleGraph V) : Type

• numContractions : ℕ
• vertexCounts : Fin (self.numContractions + 1) → ℕ
• initial_le : self.vertexCounts ⟨0, ⋯⟩ ≤ Fintype.card V
• contraction_reduces (i : Fin self.numContractions) : self.vertexCounts ⟨↑i + 1, ⋯⟩ + 2 ≤ self.vertexCounts ⟨↑i, ⋯⟩

noncomputable def SimpleGraph.sym2Endpoints {V : Type u_1} [DecidableEq V] (e : Sym2 V) : Finset V

theorem SimpleGraph.matching_edgeSet_ncard_le_card_div_two {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) : M.edgeSet.ncard ≤ Fintype.card V / 2

theorem SimpleGraph.fin_seq_le_last {n : ℕ} (f : Fin (n + 1) → ℕ) (hinc : ∀ (i : Fin n), f ⟨↑i + 1, ⋯⟩ = f ⟨↑i, ⋯⟩ + 1) : n ≤ f ⟨n, ⋯⟩

theorem SimpleGraph.edmonds_phase_bound {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (exec : G.EdmondsExecution) : exec.numPhases ≤ Fintype.card V / 2

theorem SimpleGraph.contractions_bound_of_vertex_reduction {k : ℕ} (f : Fin (k + 1) → ℕ) (n : ℕ) (hinit : f ⟨0, ⋯⟩ ≤ n) (hdecr : ∀ (i : Fin k), f ⟨↑i + 1, ⋯⟩ + 2 ≤ f ⟨↑i, ⋯⟩) : k ≤ n / 2

theorem SimpleGraph.edmonds_total_bound {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (exec : G.EdmondsExecution) : exec.numPhases * G.edgeFinset.card * (Fintype.card V / 2 + 1) ≤ Fintype.card V / 2 * G.edgeFinset.card * Fintype.card V

theorem SimpleGraph.symmDiff_edgeSet_ncard_eq {V : Type u_2} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) {u v : V} (p : G.Walk u v) (haug : p.IsAugmentingPath M) (hfin : M.edgeSet.Finite) : (symmDiffMatching M p).edgeSet.ncard = M.edgeSet.ncard + 1

theorem SimpleGraph.subgraph_edgeSet_finite {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) : M.edgeSet.Finite

theorem SimpleGraph.exists_matching_succ_ncard {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsMatching) (hnmax : ¬M.IsMaxMatching) : ∃ (M' : G.Subgraph), M'.IsMatching ∧ M'.edgeSet.ncard = M.edgeSet.ncard + 1

theorem SimpleGraph.exists_max_matching {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (M : G.Subgraph), M.IsMaxMatching

theorem SimpleGraph.exists_matching_of_size {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Mmax : G.Subgraph) (hMmax : Mmax.IsMaxMatching) (k : ℕ) (hk : k ≤ Mmax.edgeSet.ncard) : ∃ (M : G.Subgraph), M.IsMatching ∧ M.edgeSet.ncard = k

theorem SimpleGraph.edmonds_execution_exists {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (exec : G.EdmondsExecution), exec.numPhases ≤ Fintype.card V / 2

theorem SimpleGraph.edmonds_algorithm_runtime {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (M : G.Subgraph), M.IsMaxMatching ∧ ∃ numPhases ≤ Fintype.card V / 2, numPhases * G.edgeFinset.card * (Fintype.card V / 2 + 1) ≤ Fintype.card V / 2 * G.edgeFinset.card * Fintype.card V