OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedPreparedSchedule.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Prepaid shared tables followed by the concrete residue schedule

The constructor's resulting blocks are passed directly to the schedule. There is one budget, including initialization and all failed buckets.

  1. def OAI.LowSpaceSubsetSum.BudgetedPreparedSchedule.run line 19
  2. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSchedule.value line 26
  3. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSchedule.complete line 40
  4. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSchedule.account line 55
  5. theorem OAI.LowSpaceSubsetSum.BudgetedPreparedSchedule.accepts_of_core line 70