OAI/Combinatorics/LowSpaceSubsetSum/Word/WordDecisionBranches.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The two prepared branches driven by finite fair-word streams

The returned work counter measures the prepared action. The number of words read by seed generation has its own bound; generation arithmetic is separate.

  1. def OAI.LowSpaceSubsetSum.WordDecisionBranches.compressionSampler line 22
  2. def OAI.LowSpaceSubsetSum.WordDecisionBranches.representationSampler line 28
  3. abbrev OAI.LowSpaceSubsetSum.WordDecisionBranches.CompressionWords line 32
  4. abbrev OAI.LowSpaceSubsetSum.WordDecisionBranches.RepresentationWords line 33
  5. def OAI.LowSpaceSubsetSum.WordDecisionBranches.compression line 36
  6. def OAI.LowSpaceSubsetSum.WordDecisionBranches.representationAction line 40
  7. def OAI.LowSpaceSubsetSum.WordDecisionBranches.representation line 46
  8. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.representationAction_value line 52
  9. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.compression_value line 62
  10. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.representation_value line 71
  11. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.compression_sound line 84
  12. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.representation_sound line 92
  13. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.compression_probability line 102
  14. theorem OAI.LowSpaceSubsetSum.WordDecisionBranches.representation_probability line 117