OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionStreams.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Concrete compressed-group streams from their two stored arrays

  1. def OAI.LowSpaceSubsetSum.mapReader line 10
  2. theorem OAI.LowSpaceSubsetSum.mapReader_law line 13
  3. def OAI.LowSpaceSubsetSum.CompressionSetup.storedRightArray line 31
  4. abbrev OAI.LowSpaceSubsetSum.CompressionSetup.GroupState line 34
  5. def OAI.LowSpaceSubsetSum.CompressionSetup.groupStart line 40
  6. def OAI.LowSpaceSubsetSum.CompressionSetup.groupRead line 45
  7. def OAI.LowSpaceSubsetSum.CompressionSetup.groupOutput line 53
  8. theorem OAI.LowSpaceSubsetSum.CompressionSetup.groupRead_law line 59
  9. theorem OAI.LowSpaceSubsetSum.CompressionSetup.groupOutput_mem line 64
  10. def OAI.LowSpaceSubsetSum.CompressionSetup.groupKey line 82
  11. theorem OAI.LowSpaceSubsetSum.CompressionSetup.groupOutput_sorted line 86
  12. theorem OAI.LowSpaceSubsetSum.CompressionSetup.groupOutput_length line 98