Escape by a strictly increasing measure

Iterate admissible transitions to reach a prescribed lower bound for a strictly increasing measure.

theorem BGS.exists_reflTransGen_measure_ge {X : Type u} (r : X → X → Prop) (measure : X → ℕ) (target : ℕ) (step : ∀ (x : X), measure x < target → ∃ (y : X), r x y ∧ measure x < measure y) (x : X) : ∃ (y : X), Relation.ReflTransGen r x y ∧ target ≤ measure y

If every state below a target measure admits a relation step that strictly raises the measure, then finitely many such steps reach the target.