OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredDictionaryJoin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Executed bounded-list dictionary joins and semantic erasure

The callback carries the dictionary invariant on every reachable state. Erasure preserves the original trie, record order, join counters and halt flag. Reader and record semantics are specialized separately.

  1. def OAI.LowSpaceSubsetSum.StoredDictionaryJoin.erase line 19
  2. theorem OAI.LowSpaceSubsetSum.StoredDictionaryJoin.erase_empty line 22
  3. def OAI.LowSpaceSubsetSum.StoredDictionaryJoin.run line 27
  4. theorem OAI.LowSpaceSubsetSum.StoredDictionaryJoin.run_value line 35