OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationReplayCells.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete bounded-space replay of a parent tie suffix

Only the current reader and the safe dictionary survive the tail iteration. The query, report, halt, remaining-budget and work fields are preserved. The bound is independent of suffix length and remains valid on budget failure.

  1. def OAI.LowSpaceSubsetSum.RepresentationReplayCells.run line 18
  2. theorem OAI.LowSpaceSubsetSum.RepresentationReplayCells.run_value line 28
  3. theorem OAI.LowSpaceSubsetSum.RepresentationReplayCells.run_cells line 50