OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Running the prepared action on actual word-generated seeds

  1. def OAI.LowSpaceSubsetSum.WordSeedRealization.run line 13
  2. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.run_reads line 16
  3. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.run_probability line 21
  4. def OAI.LowSpaceSubsetSum.WordSeedRealization.execute line 29
  5. def OAI.LowSpaceSubsetSum.WordSeedRealization.executeCounted line 38

    Source documentation

    The action's value (which may itself contain its work counter) and the separate number of fair words read. This does not charge continuations as free machine operations.

    def executeCounted (X : Realization w N S) (action : S.Seed → β) (failure : β)
    (words : Fin N → Fin (2^w)) : β × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.WordSeedRealization.Realization

  6. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.executeCounted_value line 43
  7. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.executeCounted_reads line 47
  8. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.execute_success line 51
  9. theorem OAI.LowSpaceSubsetSum.WordSeedRealization.probability_success line 56