OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorTerminal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A prepaid terminal sort and weight match

The input lengths are cached by the preceding filter. The budget test uses only those scalar fields; both sorts and the matching loop are evaluated only after their full polynomial allowance has been reserved.

  1. def OAI.LowSpaceSubsetSum.BudgetedSeparatorTerminal.charge line 17
  2. def OAI.LowSpaceSubsetSum.BudgetedSeparatorTerminal.run line 19
  3. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorTerminal.work line 24
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorTerminal.value line 32
  5. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorTerminal.complete line 40
  6. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorTerminal.spent line 46