OAI/Combinatorics/LowSpaceSubsetSum/Storage/BudgetedPrefixCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Live memory through the interrupted depth-first prefix traversal

An overflowing dictionary is released before descending. The suspended frame retains the two bounded restriction lists, the order tail, and scalar counters. Sequential children share a single working region.

  1. abbrev OAI.LowSpaceSubsetSum.BudgetedPrefixCells.Execution line 18
  2. def OAI.LowSpaceSubsetSum.BudgetedPrefixCells.frame line 20
  3. def OAI.LowSpaceSubsetSum.BudgetedPrefixCells.run line 22
  4. theorem OAI.LowSpaceSubsetSum.BudgetedPrefixCells.value line 56
  5. theorem OAI.LowSpaceSubsetSum.BudgetedPrefixCells.cells line 85
  6. def OAI.LowSpaceSubsetSum.BudgetedPrefixCells.collect line 146
  7. theorem OAI.LowSpaceSubsetSum.BudgetedPrefixCells.collect_value line 152
  8. theorem OAI.LowSpaceSubsetSum.BudgetedPrefixCells.collect_cells line 157