OAI/Combinatorics/LowSpaceSubsetSum/Storage/TrieDictionaryCells.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Cached dictionary insertion with a live-cell trace

The caller retains the old dictionary and the input record. The trace counts only the additional trie path, key, array spine and constant local state. It uses the cached record count and freezes at the first overflowing insertion.

  1. def OAI.LowSpaceSubsetSum.TrieDictionaryCells.feed line 20
  2. theorem OAI.LowSpaceSubsetSum.TrieDictionaryCells.feed_value line 30
  3. theorem OAI.LowSpaceSubsetSum.TrieDictionaryCells.feed_cells line 37
  4. def OAI.LowSpaceSubsetSum.TrieDictionaryCells.recordedFeed line 47
  5. theorem OAI.LowSpaceSubsetSum.TrieDictionaryCells.recordedFeed_value line 53
  6. theorem OAI.LowSpaceSubsetSum.TrieDictionaryCells.recordedFeed_cells line 58
  7. def OAI.LowSpaceSubsetSum.TrieDictionaryCells.safeFeed line 65
  8. theorem OAI.LowSpaceSubsetSum.TrieDictionaryCells.safeFeed_value line 82
  9. theorem OAI.LowSpaceSubsetSum.TrieDictionaryCells.safeFeed_cells line 97