OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionPairCells.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Live cells for the two materialized compression pair lists

The recursive tail, current mapped row, append frames and output list are all included. Repeated weights remain distinct occurrences.

  1. def OAI.LowSpaceSubsetSum.CompressionPairCells.run line 13
  2. theorem OAI.LowSpaceSubsetSum.CompressionPairCells.value line 22
  3. theorem OAI.LowSpaceSubsetSum.CompressionPairCells.length line 27
  4. theorem OAI.LowSpaceSubsetSum.CompressionPairCells.cells line 30