= 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$, \b[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>.
Back to article page
