Solution (source code)

= Solution

Follow the next reference for the desired level, stopping at the tail. This returns the genuine nodes in their <linked list> order, excluding both <sentinel nodes>.
``
def nodesAt(level: Int): List[Node] = {
  require(0 <= level && level < NumLevels)
  val out = scala.collection.mutable.ListBuffer.empty[Node]
  var n = head.nexts(level)
  while (n ne tail) {
    out += n
    n = n.nexts(level)
  }
  out.toList
}
``
Write $L_h$ for the resulting <sequence> of nodes at level $h$. The <abstraction function> is
$$
\boxed{\alpha=\mathrm{map}(\mathrm{datum},L_0).}
$$
It preserves repetitions, because distinct nodes may carry equal values. A suitable <representation invariant> requires the following:

* `head` and `tail` are distinct <sentinel nodes> with the specified extreme values; every node has a `nexts` <array> of length `NumLevels`.
* For each level, following references from `head` gives a finite acyclic chain ending at `tail`, then `null`; the data along that chain are nondecreasing. Genuine values lie strictly between the <sentinel values>.
* Each $L_{h+1}$ is a subsequence of $L_h$ \b[by node identity], so the relative order of equal-valued nodes agrees across levels. Every genuine node occurs in $L_0$ and on a contiguous initial collection of levels.
* A genuine node absent from a level has `null` in that level's slot. Tail slots are all `null`; every other slot on a chain points to the next member of that chain.

These structural requirements make the traversal terminate and make descending through levels valid. A probabilistic height distribution is a performance policy, rather than a condition needed for the <abstraction function> to describe an ordered <sequence>.