OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationWeightedReader.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Reader accounting including every internal key evaluation

A supplied counted key is executed at each tournament comparison. The value refinement is unconditional; the work theorem composes its finite cost bound with the depth of the actually traversed replacement path.

  1. def OAI.LowSpaceSubsetSum.Tournament.measuredPick line 17
  2. theorem OAI.LowSpaceSubsetSum.Tournament.measuredPick_value line 25
  3. theorem OAI.LowSpaceSubsetSum.Tournament.measuredPick_work line 29
  4. def OAI.LowSpaceSubsetSum.Tournament.measuredReplace line 43
  5. theorem OAI.LowSpaceSubsetSum.Tournament.measuredReplace_value line 56
  6. theorem OAI.LowSpaceSubsetSum.Tournament.measuredReplace_work line 65
  7. def OAI.LowSpaceSubsetSum.RowMerge.measuredAdvance line 93
  8. theorem OAI.LowSpaceSubsetSum.RowMerge.measuredAdvance_value line 104
  9. theorem OAI.LowSpaceSubsetSum.RowMerge.measuredAdvance_work line 112
  10. def OAI.LowSpaceSubsetSum.MergedReader.measuredNext line 133
  11. theorem OAI.LowSpaceSubsetSum.MergedReader.measuredNext_value line 147
  12. theorem OAI.LowSpaceSubsetSum.MergedReader.measuredNext_work line 162