OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSampledAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Sequential composition of measured seed generation and a stored action

The generated seed stays resident while the prepared action runs. Generation work and action work are both charged, including the exhaustion branch.

  1. structure OAI.LowSpaceSubsetSum.WordSampledAction.Result line 19
  2. def OAI.LowSpaceSubsetSum.WordSampledAction.run line 25
  3. theorem OAI.LowSpaceSubsetSum.WordSampledAction.value line 36
  4. theorem OAI.LowSpaceSubsetSum.WordSampledAction.finite_value line 47
  5. theorem OAI.LowSpaceSubsetSum.WordSampledAction.cursor_eq line 53
  6. theorem OAI.LowSpaceSubsetSum.WordSampledAction.cursor_le line 61
  7. theorem OAI.LowSpaceSubsetSum.WordSampledAction.bounded line 68