OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorNode.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Prepaid filter nodes with cached output lengths

The successful node retains only filtered lists and two scalar lengths. Its whole filtering, length computation and branch bookkeeping is reserved before either interval predicate is evaluated.

  1. structure OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.Frame line 17
  2. def OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.prepare line 25
  3. def OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.charge line 33
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.prepare_work line 35
  5. def OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.run line 55
  6. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.work line 62
  7. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.spent line 72
  8. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.value line 84
  9. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorNode.complete line 93