OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationReaderCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Scratch of a concrete representation reader

The array cursor performs one indexed load. Tournament replacement uses the measured list-mask key and retains the shared right array without copying it. Every output includes the unchanged work counter as well as the live trace.

  1. def OAI.LowSpaceSubsetSum.RepresentationReaderCells.rowRead line 17
  2. theorem OAI.LowSpaceSubsetSum.RepresentationReaderCells.rowRead_value line 25
  3. theorem OAI.LowSpaceSubsetSum.RepresentationReaderCells.rowRead_cells line 30
  4. theorem OAI.LowSpaceSubsetSum.RepresentationReaderCells.reader line 35
  5. def OAI.LowSpaceSubsetSum.RepresentationReaderCells.read line 40
  6. theorem OAI.LowSpaceSubsetSum.RepresentationReaderCells.read_value line 48
  7. theorem OAI.LowSpaceSubsetSum.RepresentationReaderCells.read_cells line 57
  8. theorem OAI.LowSpaceSubsetSum.RepresentationReaderCells.read_scale line 68