OAI/Combinatorics/LowSpaceSubsetSum/Storage/TrieCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Extra live cells of fixed-width trie lookup and insertion

The old trie is retained by the caller. Insertion allocates one new path and shares all untouched subtrees; this trace counts that path and its recursive frames, rather than duplicating the whole trie at every level.

  1. def OAI.LowSpaceSubsetSum.TrieCells.contains line 16
  2. theorem OAI.LowSpaceSubsetSum.TrieCells.contains_value line 25
  3. theorem OAI.LowSpaceSubsetSum.TrieCells.contains_cells line 31
  4. def OAI.LowSpaceSubsetSum.TrieCells.insert line 44
  5. theorem OAI.LowSpaceSubsetSum.TrieCells.insert_value line 57
  6. theorem OAI.LowSpaceSubsetSum.TrieCells.insert_cells line 65