OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorCells.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Live buffers in every interrupted separator traversal

The execution below follows the same guarded calls and result branches as BudgetedSeparatorTraversal.execute. Its additional field counts the retained list/continuation cells. scratch accounts separately for the interval-query callback's temporary cells. Entry payloads and incidence tables remain shared. Sequential children retain only a Boolean result.

  1. abbrev OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.Execution line 18
  2. def OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.seq line 22
  3. def OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.scope line 29
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.seq_value line 36
  5. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.scope_value line 41
  6. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.seq_cells line 46
  7. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.scope_cells line 54
  8. def OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.run line 63
  9. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.run_value line 84
  10. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.child_size line 107
  11. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCells.run_cells line 117