OAI/Combinatorics/LowSpaceSubsetSum/Storage/BudgetedReplayCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Tail replay with a live-cell trace

The trace includes the reader before and after a fetch, the current record, and both callback states during reporting. Only their successors survive the tail call. Scratch returned by the concrete primitive calls is kept separate.

  1. def OAI.LowSpaceSubsetSum.BudgetedReplayCells.loop line 17
  2. theorem OAI.LowSpaceSubsetSum.BudgetedReplayCells.loop_value line 51
  3. theorem OAI.LowSpaceSubsetSum.BudgetedReplayCells.loop_cells line 77
  4. def OAI.LowSpaceSubsetSum.BudgetedReplayCells.run line 125
  5. theorem OAI.LowSpaceSubsetSum.BudgetedReplayCells.run_value line 132
  6. theorem OAI.LowSpaceSubsetSum.BudgetedReplayCells.run_cells line 143