OAI/Combinatorics/LowSpaceSubsetSum/Streams/DistinctStreamCount.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Counting distinct keys without materializing the output stream

The mutable state consists of a reader state, one previous key and a count. Sorted keys make adjacent duplicate removal exact. The second component of the result counts actual reader calls, including a final unsuccessful call.

  1. def OAI.LowSpaceSubsetSum.DistinctStreamCount.tail line 17
  2. def OAI.LowSpaceSubsetSum.DistinctStreamCount.run line 30
  3. theorem OAI.LowSpaceSubsetSum.DistinctStreamCount.tail_queries line 39
  4. theorem OAI.LowSpaceSubsetSum.DistinctStreamCount.run_queries line 52
  5. theorem OAI.LowSpaceSubsetSum.DistinctStreamCount.tail_value line 62
  6. theorem OAI.LowSpaceSubsetSum.DistinctStreamCount.run_value line 91