OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedSnapshot.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conditional prepaid snapshots

The caller charges its fixed control overhead; this stage reserves only the snapshot allowance, and never clones a cursor after a failed comparison.

  1. def OAI.LowSpaceSubsetSum.BudgetedSnapshot.execute line 16
  2. theorem OAI.LowSpaceSubsetSum.BudgetedSnapshot.value line 25
  3. theorem OAI.LowSpaceSubsetSum.BudgetedSnapshot.work line 36
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSnapshot.spent line 45
  5. theorem OAI.LowSpaceSubsetSum.BudgetedSnapshot.complete line 59
  6. theorem OAI.LowSpaceSubsetSum.BudgetedSnapshot.remaining line 69