OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedTieStep.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A prepaid callback for one outer tie occurrence

  1. def OAI.LowSpaceSubsetSum.BudgetedTieStep.result line 13
  2. def OAI.LowSpaceSubsetSum.BudgetedTieStep.execute line 18
  3. def OAI.LowSpaceSubsetSum.BudgetedTieStep.bill line 29
  4. theorem OAI.LowSpaceSubsetSum.BudgetedTieStep.execute_value line 36
  5. theorem OAI.LowSpaceSubsetSum.BudgetedTieStep.execute_work line 55
  6. theorem OAI.LowSpaceSubsetSum.BudgetedTieStep.execute_spent line 69
  7. theorem OAI.LowSpaceSubsetSum.BudgetedTieStep.execute_complete line 96