OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedRejectionExecution.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Counted rejection returning the successful sampler seed

The full candidate buffer is produced once from the word stream and tested by the tail rejection loop. The accepted value supplies the unused backup coordinate. Generation work, evaluator work and peak storage are explicit; no execution cost is assigned to arbitrary program continuations.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.program_run_bind line 20
  2. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.program_run_map line 31
  3. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.tuple_run line 38
  4. def OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.attach line 61
  5. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.attach_eq line 68
  6. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.tested_value line 95
  7. structure OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.Trace line 104
  8. def OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.run line 112
  9. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.run_seed line 122
  10. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.run_cursor line 133
  11. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.program_value line 137
  12. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.tested_bounds line 148
  13. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.run_work line 157
  14. theorem OAI.LowSpaceSubsetSum.WordSeedRejectionExecution.run_cells line 166