OAI/Combinatorics/LowSpaceSubsetSum/Storage/BudgetedCheckerCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Full interrupted-checker buffer lifetime

The header, the interval traversal and the terminal run in the same order as the budgeted checker. The added peak field accounts for live temporary lists and continuation cells; shared entry payloads and tables are external.

  1. def OAI.LowSpaceSubsetSum.BudgetedCheckerCells.run line 21
  2. theorem OAI.LowSpaceSubsetSum.BudgetedCheckerCells.run_value line 36
  3. def OAI.LowSpaceSubsetSum.BudgetedCheckerCells.bound line 56
  4. theorem OAI.LowSpaceSubsetSum.BudgetedCheckerCells.run_cells line 60
  5. def OAI.LowSpaceSubsetSum.BudgetedCheckerCells.arrays line 87
  6. theorem OAI.LowSpaceSubsetSum.BudgetedCheckerCells.arrays_value line 93
  7. theorem OAI.LowSpaceSubsetSum.BudgetedCheckerCells.arrays_cells line 99
  8. theorem OAI.LowSpaceSubsetSum.BudgetedCheckerCells.bound_le line 110