= Solution
Each of the finitely many distinct values has a first occurrence at a finite position, so every one is eventually emitted. After the last new value, however, the <list filters> keep searching the remaining infinite input for another new value. They never observe a terminating `[]`. Therefore the result has a finite visible prefix followed by the <bottom value>:
$$
\boxed{x_1:x_2:\cdots:x_k:\bot,\qquad\text{rather than }[x_1,\ldots,x_k].}
$$
For example, `remalldups (repeat 1)` exposes `1 : ...`, but demanding its tail diverges. This is the <absence-detection obstruction for infinite lists>: no finite inspection can certify that an unseen new value will never occur. The emitted values are correct, but computing the output length or proving the output empty after its last value does not terminate.
Back to article page
