-- Maclain Hunter: Loop Halting Guarantee
-- Exact authored source SHA-256: d317154a15be0a16f2474591c1599951ad98b9d245112b7223256dcb541b2125
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

def iterations {α : Type} (step : α → Option α) : Nat → α → Nat
  | 0, _ => 0
  | n + 1, s =>
    match step s with
    | none => 0
    | some t => iterations step n t + 1
theorem fuel_iteration_bound {α : Type} (step : α → Option α) (fuel : Nat) (s : α) :
    iterations step fuel s ≤ fuel := by
  induction fuel generalizing s with
  | zero => exact Nat.le_refl 0
  | succ n ih =>
    cases h : step s with
    | none =>
      unfold iterations
      rw [h]
      exact Nat.zero_le (n + 1)
    | some t =>
      unfold iterations
      rw [h]
      exact Nat.succ_le_succ (ih t)
#print axioms fuel_iteration_bound

end HunterAuthored