OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedSchedule.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The concrete shared-budget residue schedule

  1. def OAI.LowSpaceSubsetSum.BudgetedSchedule.run line 13
  2. theorem OAI.LowSpaceSubsetSum.BudgetedSchedule.reference_eq line 20
  3. theorem OAI.LowSpaceSubsetSum.BudgetedSchedule.value line 29
  4. def OAI.LowSpaceSubsetSum.BudgetedSchedule.allowance line 48
  5. theorem OAI.LowSpaceSubsetSum.BudgetedSchedule.complete line 54