OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionReader.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Measured shared-array readers for the compression branch

  1. abbrev OAI.LowSpaceSubsetSum.CompressionReader.key line 10
  2. abbrev OAI.LowSpaceSubsetSum.CompressionReader.State line 13
  3. theorem OAI.LowSpaceSubsetSum.CompressionReader.row_reader line 16
  4. def OAI.LowSpaceSubsetSum.CompressionReader.read line 21
  5. theorem OAI.LowSpaceSubsetSum.CompressionReader.read_value line 27
  6. theorem OAI.LowSpaceSubsetSum.CompressionReader.read_work line 47
  7. theorem OAI.LowSpaceSubsetSum.CompressionReader.read_scale line 55
  8. def OAI.LowSpaceSubsetSum.CompressionReader.scalarKey line 63
  9. theorem OAI.LowSpaceSubsetSum.CompressionReader.scalarKey_work line 68
  10. def OAI.LowSpaceSubsetSum.CompressionReader.snapshot line 71
  11. theorem OAI.LowSpaceSubsetSum.CompressionReader.snapshot_value line 77
  12. theorem OAI.LowSpaceSubsetSum.CompressionReader.snapshot_work line 82
  13. theorem OAI.LowSpaceSubsetSum.CompressionReader.groupRead_value line 88