OAI/Combinatorics/LowSpaceSubsetSum/Streams/CountedTrie.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Counted trie operations and a cached distinct-key count

The capacity test uses the cached count. It does not traverse the whole trie to recompute entries after insertion. Equality to the dictionary specification follows from the fixed-width insertion theorem.

  1. def OAI.LowSpaceSubsetSum.CountedTrie.contains line 16
  2. theorem OAI.LowSpaceSubsetSum.CountedTrie.contains_value line 25
  3. theorem OAI.LowSpaceSubsetSum.CountedTrie.contains_work line 31
  4. def OAI.LowSpaceSubsetSum.CountedTrie.insert line 41
  5. theorem OAI.LowSpaceSubsetSum.CountedTrie.insert_value line 54
  6. theorem OAI.LowSpaceSubsetSum.CountedTrie.insert_work line 60
  7. structure OAI.LowSpaceSubsetSum.CountedTrie.Cached line 66
  8. def OAI.LowSpaceSubsetSum.CountedTrie.feed line 70
  9. theorem OAI.LowSpaceSubsetSum.CountedTrie.feed_work line 78
  10. theorem OAI.LowSpaceSubsetSum.CountedTrie.feed_state line 87
  11. theorem OAI.LowSpaceSubsetSum.CountedTrie.feed_count line 104