OAI/Combinatorics/LowSpaceSubsetSum/Separators/BudgetedSeparatorFlow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Sequencing the already charged checker operations

The enclosing node charge includes branch bookkeeping. These combinators add only the work counters of their constituent charged operations.

  1. def OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.pure line 17
  2. def OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.bind line 19
  3. def OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.Account line 26
  4. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.pure_account line 30
  5. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.bind_account line 38
  6. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.bind_eq_some line 63
  7. theorem OAI.LowSpaceSubsetSum.BudgetedSeparatorFlow.bind_complete line 78