OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedHistory.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The whole dependent representation history retains successful seeds

  1. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.clog_le line 11
  2. def OAI.LowSpaceSubsetSum.WordSeedRealization.partitions line 14
  3. def OAI.LowSpaceSubsetSum.WordSeedRealization.nested line 23
  4. def OAI.LowSpaceSubsetSum.WordSeedRealization.residues line 28
  5. def OAI.LowSpaceSubsetSum.WordSeedRealization.extraPrime line 38
  6. def OAI.LowSpaceSubsetSum.WordSeedRealization.guessHistory line 44
  7. def OAI.LowSpaceSubsetSum.WordSeedRealization.partitionHistory line 53
  8. def OAI.LowSpaceSubsetSum.WordSeedRealization.primeHistory line 58
  9. def OAI.LowSpaceSubsetSum.WordSeedRealization.trialHistory line 63
  10. def OAI.LowSpaceSubsetSum.WordSeedRealization.extraHistory line 70
  11. def OAI.LowSpaceSubsetSum.WordSeedRealization.separatorDraws line 79
  12. def OAI.LowSpaceSubsetSum.WordSeedRealization.bucketHistory line 86