 Solution

The representation invariant says that root is either null or the root of a finite, acyclic binary search tree, with no software object shared between different child subtrees. Every reachable entry has a non-null word and a strictly positive frequency. For each entry $t$, every word in its entire left subtree is strictly less than t.word, and every word in its entire right subtree is strictly greater. This is an inherited ordering condition on all descendants, rather than merely a comparison with immediate children. It implies that each distinct word has exactly one entry. The empty initial state satisfies it.

The abstraction function is the finite multiset assigning each stored word its positive count and assigning all other words zero. Frequencies and their increments must fit in Int; the implementation below explicitly rejects an increment at its representational limit instead of silently violating positivity through integer overflow.