OAI/Combinatorics/LowSpaceSubsetSum/Streams/CountedDictionaryCallback.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Counted dictionary callbacks with an intrinsic trie invariant

The executable state carries the proved width/count invariant. Encoding is computed once per emitted record, and its work plus record copying is included.

  1. def OAI.LowSpaceSubsetSum.CountedDictionaryCallback.SafeState line 16
  2. def OAI.LowSpaceSubsetSum.CountedDictionaryCallback.empty line 20
  3. def OAI.LowSpaceSubsetSum.CountedDictionaryCallback.feed line 23
  4. theorem OAI.LowSpaceSubsetSum.CountedDictionaryCallback.feed_value line 34
  5. theorem OAI.LowSpaceSubsetSum.CountedDictionaryCallback.feed_work line 41
  6. def OAI.LowSpaceSubsetSum.CountedDictionaryCallback.callback line 54
  7. theorem OAI.LowSpaceSubsetSum.CountedDictionaryCallback.callback_value line 65
  8. theorem OAI.LowSpaceSubsetSum.CountedDictionaryCallback.callback_work line 75