OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedMeasured.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Measured seed generation with cached accepted outputs

Dependent continuations use the stored output of the preceding call. The equality with its ideal value is used only for type transport. A map must provide an actual measured evaluator; its work is added explicitly.

  1. structure OAI.LowSpaceSubsetSum.WordSeedMeasured.Accepted line 19
  2. structure OAI.LowSpaceSubsetSum.WordSeedMeasured.Result line 24
  3. structure OAI.LowSpaceSubsetSum.WordSeedMeasured.Execution line 31
  4. def OAI.LowSpaceSubsetSum.WordSeedMeasured.Execution.Bounded line 37
  5. def OAI.LowSpaceSubsetSum.WordSeedMeasured.pure line 42
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.pure_bounded line 46
  7. def OAI.LowSpaceSubsetSum.WordSeedMeasured.mapAccepted line 49
  8. def OAI.LowSpaceSubsetSum.WordSeedMeasured.mapRun line 55
  9. def OAI.LowSpaceSubsetSum.WordSeedMeasured.map line 66
  10. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.map_bounded line 76
  11. def OAI.LowSpaceSubsetSum.WordSeedMeasured.pairAccepted line 93
  12. def OAI.LowSpaceSubsetSum.WordSeedMeasured.bindRun line 104
  13. def OAI.LowSpaceSubsetSum.WordSeedMeasured.bind line 116
  14. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.bind_bounded line 135