OAI/Combinatorics/LowSpaceSubsetSum/Word/WordRepresentationHistory.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact word programs for the complete dependent representation history

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