OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionFromPermutation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compression execution from a stored permutation array

Domain construction is prepaid and its returned index lists are passed directly into weight generation. No permutation oracle is used by the run.

  1. def OAI.LowSpaceSubsetSum.CompressionFromPermutation.finish line 17
  2. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutation.finish_source line 27
  3. def OAI.LowSpaceSubsetSum.CompressionFromPermutation.charge line 32
  4. def OAI.LowSpaceSubsetSum.CompressionFromPermutation.run line 34
  5. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutation.account line 39
  6. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutation.sound line 53
  7. theorem OAI.LowSpaceSubsetSum.CompressionFromPermutation.accepts line 61