OAI/Combinatorics/LowSpaceSubsetSum/Storage/BudgetedOuterCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Live cells of a tail replay with a prepaid inner callback

The callback may exhaust its remaining allowance. Its scratch trace is added to the retained reader, current record and user state before the next tail iteration, and failure drops all local continuations.

  1. def OAI.LowSpaceSubsetSum.BudgetedOuterCells.loop line 17
  2. theorem OAI.LowSpaceSubsetSum.BudgetedOuterCells.loop_value line 56
  3. theorem OAI.LowSpaceSubsetSum.BudgetedOuterCells.loop_cells line 87
  4. def OAI.LowSpaceSubsetSum.BudgetedOuterCells.run line 141
  5. theorem OAI.LowSpaceSubsetSum.BudgetedOuterCells.run_value line 148
  6. theorem OAI.LowSpaceSubsetSum.BudgetedOuterCells.run_cells line 159