OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationPrefixArrays.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The stored layout, guesses and balanced partitions of one trial

All three stages stop on exhaustion. The dependent seed's ideal layout is used only as a type index for the partition sampler, whose actual code is the fixed sequence of bounded integer draws and array scans.

  1. structure OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.Data line 18
  2. def OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.run line 23
  3. theorem OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.layout_none_iff line 36
  4. theorem OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.none_iff line 54
  5. theorem OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.complete line 82
  6. theorem OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.components line 93
  7. theorem OAI.LowSpaceSubsetSum.RepresentationPrefixArrays.work line 112