OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedConstructors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Successful seed constructors for products and bounded rejection

The rejection constructor draws and retains the full candidate tuple. Its backup coordinate is the accepted value, so no backup word is read.

  1. def OAI.LowSpaceSubsetSum.WordSeedRealization.enlarge line 18
  2. def OAI.LowSpaceSubsetSum.WordSeedRealization.prod line 26
  3. def OAI.LowSpaceSubsetSum.WordSeedRealization.pi line 31
  4. def OAI.LowSpaceSubsetSum.WordSeedRealization.rejectionSeed line 45
  5. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.rejectionSeed_observe line 51
  6. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.rejectionSeed_candidates line 59
  7. def OAI.LowSpaceSubsetSum.WordSeedRealization.rejection line 69