OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedReplay.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cost-carrying tie-suffix replay

Every performed reader, key and callback evaluation contributes its own counter. The result is exactly the bounded replay. The work bound uses its actual stopped query/report counts, rather than the supplied fuel.

  1. def OAI.LowSpaceSubsetSum.CountedReplay.runAcc line 17
  2. theorem OAI.LowSpaceSubsetSum.CountedReplay.runAcc_value line 37
  3. theorem OAI.LowSpaceSubsetSum.CountedReplay.runAcc_work line 56
  4. def OAI.LowSpaceSubsetSum.CountedReplay.run line 86
  5. theorem OAI.LowSpaceSubsetSum.CountedReplay.run_value line 90
  6. theorem OAI.LowSpaceSubsetSum.CountedReplay.run_work line 96