OAI/Combinatorics/LowSpaceSubsetSum/Search/BudgetedTieOuter.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Prepaid outer traversal of a Cartesian tie group

  1. def OAI.LowSpaceSubsetSum.BudgetedTieOuter.execute line 13
  2. def OAI.LowSpaceSubsetSum.BudgetedTieOuter.reference line 23
  3. theorem OAI.LowSpaceSubsetSum.BudgetedTieOuter.execute_value line 31
  4. theorem OAI.LowSpaceSubsetSum.BudgetedTieOuter.execute_work line 48
  5. theorem OAI.LowSpaceSubsetSum.BudgetedTieOuter.execute_spent line 68
  6. def OAI.LowSpaceSubsetSum.BudgetedTieOuter.potential line 89
  7. def OAI.LowSpaceSubsetSum.BudgetedTieOuter.allowance line 92
  8. theorem OAI.LowSpaceSubsetSum.BudgetedTieOuter.allowance_le line 103
  9. theorem OAI.LowSpaceSubsetSum.BudgetedTieOuter.execute_complete line 143