OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorRemaining.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact allowance spending by completed separator calls

  1. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorTraversal.remaining line 13
  2. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorCheck.remaining line 75