OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredSort.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Mergesort including every comparator callback

The value agrees exactly with the counted merge and sort. The work theorem scales its structural ledger by a bound on the supplied comparison work.

  1. def OAI.LowSpaceSubsetSum.MeasuredSort.merge line 15
  2. theorem OAI.LowSpaceSubsetSum.MeasuredSort.merge_value line 29
  3. theorem OAI.LowSpaceSubsetSum.MeasuredSort.merge_work line 39
  4. def OAI.LowSpaceSubsetSum.MeasuredSort.run line 59
  5. theorem OAI.LowSpaceSubsetSum.MeasuredSort.run_value line 71
  6. theorem OAI.LowSpaceSubsetSum.MeasuredSort.run_work line 83
  7. def OAI.LowSpaceSubsetSum.MeasuredSort.sort line 112
  8. theorem OAI.LowSpaceSubsetSum.MeasuredSort.sort_value line 115
  9. theorem OAI.LowSpaceSubsetSum.MeasuredSort.sort_work line 120