OAI/Combinatorics/LowSpaceSubsetSum/Counting/CountedReplayPotential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Telescoping callback costs through a stopped replay

The callback may itself contain a replay. A potential on its returned state charges that actual inner work; a uniform worst-case inner fuel bound is not multiplied by the outer stream length.

  1. theorem OAI.LowSpaceSubsetSum.CountedReplay.runAcc_work_potential line 17
  2. theorem OAI.LowSpaceSubsetSum.CountedReplay.run_work_potential line 46