OAI/Combinatorics/LowSpaceSubsetSum/Counting/GuessArrayExecution.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Three bounded interval draws stored as a small integer array

  1. def OAI.LowSpaceSubsetSum.GuessArrayExecution.coupling line 12
  2. def OAI.LowSpaceSubsetSum.GuessArrayExecution.execution line 16
  3. theorem OAI.LowSpaceSubsetSum.GuessArrayExecution.execution_bounded line 19
  4. def OAI.LowSpaceSubsetSum.GuessArrayExecution.run line 26
  5. theorem OAI.LowSpaceSubsetSum.GuessArrayExecution.value line 30
  6. theorem OAI.LowSpaceSubsetSum.GuessArrayExecution.work line 34