OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedReplayLoops.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tail-recursive implementations of prepaid inner loops

The accumulated work counter removes return frames while retaining exactly the measured semantics used in the correctness proofs.

  1. def OAI.LowSpaceSubsetSum.BudgetedReplayLoop.loop line 17
  2. theorem OAI.LowSpaceSubsetSum.BudgetedReplayLoop.loop_eq line 41
  3. def OAI.LowSpaceSubsetSum.BudgetedReplayLoop.execute line 65
  4. theorem OAI.LowSpaceSubsetSum.BudgetedReplayLoop.execute_eq line 69
  5. def OAI.LowSpaceSubsetSum.BudgetedFillLoop.loop line 81
  6. theorem OAI.LowSpaceSubsetSum.BudgetedFillLoop.loop_eq line 101
  7. def OAI.LowSpaceSubsetSum.BudgetedFillLoop.execute line 124
  8. theorem OAI.LowSpaceSubsetSum.BudgetedFillLoop.execute_eq line 129