OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedBucket.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Retaining one left dictionary during the guarded right-prefix search

  1. def OAI.LowSpaceSubsetSum.BudgetedBucket.run line 14
  2. theorem OAI.LowSpaceSubsetSum.BudgetedBucket.value line 27
  3. theorem OAI.LowSpaceSubsetSum.BudgetedBucket.account line 90
  4. def OAI.LowSpaceSubsetSum.BudgetedBucket.allowance line 120
  5. theorem OAI.LowSpaceSubsetSum.BudgetedBucket.complete line 129
  6. theorem OAI.LowSpaceSubsetSum.BudgetedBucket.remaining line 165