OAI/Combinatorics/LowSpaceSubsetSum/Streams/BufferReplay.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Reporting the stored part of a tie group

The immutable buffer is traversed by one natural index. The same bounded reporter used for a generator suffix applies, so buffer reporting shares the all-outcome stop and query bounds without keeping an output list.

  1. def OAI.LowSpaceSubsetSum.BufferReplay.read line 21
  2. def OAI.LowSpaceSubsetSum.BufferReplay.view line 24
  3. theorem OAI.LowSpaceSubsetSum.BufferReplay.isReader line 26
  4. def OAI.LowSpaceSubsetSum.BufferReplay.run line 39
  5. theorem OAI.LowSpaceSubsetSum.BufferReplay.queries_le line 42
  6. theorem OAI.LowSpaceSubsetSum.BufferReplay.reports_le line 46
  7. theorem OAI.LowSpaceSubsetSum.BufferReplay.state_complete line 55
  8. theorem OAI.LowSpaceSubsetSum.BufferReplay.filled_buffer_keys line 67