OAI/Combinatorics/LowSpaceSubsetSum/Streams/CountedRecordedDictionary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Recorded dictionary feed using its cached array length

The record array's length is the exact number of distinct keys. The runtime capacity comparison uses this scalar rather than traversing the trie. Key encoding and the emitter are charged by their callers.

  1. def OAI.LowSpaceSubsetSum.CountedTrie.recordedFeed line 17
  2. theorem OAI.LowSpaceSubsetSum.CountedTrie.recordedFeed_work line 23
  3. theorem OAI.LowSpaceSubsetSum.CountedTrie.recordedFeed_value line 28
  4. def OAI.LowSpaceSubsetSum.CountedTrie.recordedFold line 44
  5. theorem OAI.LowSpaceSubsetSum.CountedTrie.recordedFold_value line 52
  6. theorem OAI.LowSpaceSubsetSum.CountedTrie.recordedFold_work line 64