OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionReaderCells.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Concrete compression reader and snapshot storage

Each tournament front contains two scalar weights and one bounded cursor. The shared right array is retained by the caller and is never copied by a read or a snapshot.

  1. def OAI.LowSpaceSubsetSum.CompressionReaderCells.rowRead line 16
  2. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.rowRead_value line 23
  3. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.rowRead_cells line 27
  4. def OAI.LowSpaceSubsetSum.CompressionReaderCells.pairKey line 31
  5. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.reader line 34
  6. def OAI.LowSpaceSubsetSum.CompressionReaderCells.read line 39
  7. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.read_value line 46
  8. def OAI.LowSpaceSubsetSum.CompressionReaderCells.stateCells line 56
  9. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.stateCells_exact line 59
  10. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.read_cells line 63
  11. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.read_scale line 73
  12. def OAI.LowSpaceSubsetSum.CompressionReaderCells.scalarKey line 93
  13. def OAI.LowSpaceSubsetSum.CompressionReaderCells.snapshot line 96
  14. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.snapshot_value line 105
  15. theorem OAI.LowSpaceSubsetSum.CompressionReaderCells.snapshot_cells line 110