OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorArrays.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Guarded array-to-list entry to the prepared checker

The dictionary arrays and prepared tables remain shared. Conversion to temporary pointer lists is prepaid using the two constant-time array sizes. No temporary list is created on the insufficient-budget branch.

  1. def OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.conversionCharge line 19
  2. def OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.convert line 22
  3. def OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.execute line 27
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.account line 33
  5. def OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.allowance line 44
  6. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.complete line 49
  7. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.value line 65
  8. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.remaining line 77
  9. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorArrays.allowance_scale line 89