OAI/Combinatorics/LowSpaceSubsetSum/Streams/MeasuredDistinctCount.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Tail-recursive distinct counting with measured reader calls

Only the current reader state, previous key, count, remaining fuel and work counter survive each iteration. No list of emitted keys is constructed.

  1. def OAI.LowSpaceSubsetSum.MeasuredDistinctCount.loop line 15
  2. theorem OAI.LowSpaceSubsetSum.MeasuredDistinctCount.loop_value line 28
  3. theorem OAI.LowSpaceSubsetSum.MeasuredDistinctCount.loop_work line 58
  4. def OAI.LowSpaceSubsetSum.MeasuredDistinctCount.run line 77
  5. theorem OAI.LowSpaceSubsetSum.MeasuredDistinctCount.run_value line 80
  6. theorem OAI.LowSpaceSubsetSum.MeasuredDistinctCount.run_work line 85