OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationBackgroundPreparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Materializing the eight allocated background lists

The outside domain is scanned and sorted, the six binomial widths determine the eight sizes, and the consecutive rows are copied from that domain. The size check makes every array access valid on every input execution.

  1. def OAI.LowSpaceSubsetSum.RepresentationBackgroundPreparation.run line 19
  2. theorem OAI.LowSpaceSubsetSum.RepresentationBackgroundPreparation.run_of_size line 29
  3. theorem OAI.LowSpaceSubsetSum.RepresentationBackgroundPreparation.work line 40
  4. theorem OAI.LowSpaceSubsetSum.RepresentationBackgroundPreparation.lengths line 56