OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionContextCells.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Preparing a shared compression reader context

Sort the right array once, then initialize rows by reading that same array. The trace includes the old array, list view and returned sorted array, as well as the direct tournament construction.

  1. def OAI.LowSpaceSubsetSum.CompressionContextCells.compare line 18
  2. def OAI.LowSpaceSubsetSum.CompressionContextCells.sort line 21
  3. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.sort_value line 25
  4. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.sort_size line 30
  5. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.sort_cells line 33
  6. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.primary line 53
  7. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.secondary line 58
  8. def OAI.LowSpaceSubsetSum.CompressionContextCells.fromArrays line 63
  9. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.fromArrays_value line 70
  10. def OAI.LowSpaceSubsetSum.CompressionContextCells.build line 78
  11. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.build_value line 84
  12. theorem OAI.LowSpaceSubsetSum.CompressionContextCells.build_cells line 88