OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionArrayWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Work of constructing the compression trial's shared arrays

  1. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.source_lengths line 12
  2. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.compact_work_source line 32
  3. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.compact_lengths_source line 46
  4. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.raw_work_source line 61
  5. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.assemble_work_source line 77
  6. theorem OAI.LowSpaceSubsetSum.CompressionArrayBuild.run_work_source line 124