OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredPrefixExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Depth-first prefix execution retaining bounded stored records

The collector result is inspected in place. Overflow discards it before either recursive child is entered; an accepting first child skips the second child. Only the proof view maps the stored masks to finite sets.

  1. def OAI.LowSpaceSubsetSum.StoredPrefixExecution.run line 17
  2. def OAI.LowSpaceSubsetSum.StoredPrefixExecution.fullCost line 34
  3. theorem OAI.LowSpaceSubsetSum.StoredPrefixExecution.run_work line 46
  4. theorem OAI.LowSpaceSubsetSum.StoredPrefixExecution.run_value line 60
  5. theorem OAI.LowSpaceSubsetSum.StoredPrefixExecution.fullCost_le_ledger line 84
  6. def OAI.LowSpaceSubsetSum.StoredPrefixExecution.taskCollector line 126
  7. theorem OAI.LowSpaceSubsetSum.StoredPrefixExecution.taskCollector_value line 132
  8. theorem OAI.LowSpaceSubsetSum.StoredPrefixExecution.taskCollector_work line 142
  9. theorem OAI.LowSpaceSubsetSum.StoredPrefixExecution.run_tasks_work line 160