= Solution
The <representation invariant> is
$$
\boxed{p\ne\mathrm{NIL},\quad p.\mathrm{count}=|\alpha(p.\mathrm{tail})|\geq0,\quad p.\mathrm{tail}\text{ is a finite acyclic chain excluding }p.}
$$
Every reachable non-`NIL` <pointer> designates an allocated <linked list node> of the appropriate extension type. The header is not a data element. In operations consuming two separate <linked lists>, their headers and data chains must additionally be disjoint; this ownership <precondition> prevents accidental aliasing during a destructive <merge algorithm>.
Back to article page
