OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorCheck.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fully budgeted checker on the four prepared blocks

Cached lengths drive every guard. The terminal sort, each pair of filters, and the next block are reached only after their allowances are available. The callback result carries the unspent allowance into the next branch.

  1. def OAI.LowSpaceSubsetSum.BudgetedSeparatorCheck.header line 20
  2. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCheck.header_account line 23
  3. def OAI.LowSpaceSubsetSum.BudgetedSeparatorCheck.execute line 28
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCheck.account line 43
  5. def OAI.LowSpaceSubsetSum.BudgetedSeparatorCheck.reference line 69