OAI/Combinatorics/LowSpaceSubsetSum/Storage/IntervalDomainExecution.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic scans for the fixed input-index domains

The actual scan tests two integer inequalities. The Finsets used in the probability argument are not stored or searched by the executable scan. Both values and charged work agree with the finite-set domain specification.

  1. def OAI.LowSpaceSubsetSum.IntervalDomainExecution.positions line 18
  2. def OAI.LowSpaceSubsetSum.IntervalDomainExecution.run line 21
  3. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.positions_source line 26
  4. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.source line 31
  5. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.work line 35
  6. def OAI.LowSpaceSubsetSum.IntervalDomainExecution.mixers line 40
  7. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.mixers_source line 48
  8. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.mixers_work line 53
  9. def OAI.LowSpaceSubsetSum.IntervalDomainExecution.rightStart line 59
  10. def OAI.LowSpaceSubsetSum.IntervalDomainExecution.rightLength line 63
  11. def OAI.LowSpaceSubsetSum.IntervalDomainExecution.compression line 67
  12. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.compression_source line 75
  13. theorem OAI.LowSpaceSubsetSum.IntervalDomainExecution.compression_work line 84