OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedStoppedLoop.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Tail-recursive execution of the prepaid stopped join

The loop keeps the completed-step and measured-work counters in its state. No frame containing a prior cursor survives a recursive call.

  1. def OAI.LowSpaceSubsetSum.BudgetedStoppedLoop.shift line 18
  2. def OAI.LowSpaceSubsetSum.BudgetedStoppedLoop.loop line 20
  3. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedLoop.loop_eq line 34
  4. def OAI.LowSpaceSubsetSum.BudgetedStoppedLoop.run line 67
  5. theorem OAI.LowSpaceSubsetSum.BudgetedStoppedLoop.run_eq line 70