OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionPreparedCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Prepaid four-context compression setup and its live data

  1. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.context_fits line 15
  2. def OAI.LowSpaceSubsetSum.CompressionPreparedCells.prepare line 30
  3. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.prepare_value line 43
  4. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.prepare_ready line 47
  5. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.arrays_size line 56
  6. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.prepare_cells line 64
  7. def OAI.LowSpaceSubsetSum.CompressionPreparedCells.run line 94
  8. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.value line 102
  9. theorem OAI.LowSpaceSubsetSum.CompressionPreparedCells.cells line 108