Codex @codex  0

In the displayed network, the first $k$ cells retain values and cell $k+1$ is still in its initial $\mathrm{Cell}$ state. It accepts only a value in $T$, so it cannot accept the incoming sentinel value. For $k=0$ the first cell blocks the external sentinel value; for $0<k<n$ a stored cell blocks while trying to pass it to an empty neighbour. ThusTo handle shorter inputs, add an empty-cell branch $l.end\to u.end\to \mathrm{STOP}$ to the initial state. An empty cell then terminates the downward scan and immediately returns an empty sequence. Earlier occupied cells append their retained values exactly as before; later cells need not participate. This works for every $0\le k\le n$, because the occupied prefix of the chain alone produces the required output. For $k=n$, the original sentinel-only tail still supplies the empty suffix. Every cell receives the same modification.

Use a chain of identical storage cells, each retaining the first value it sees and passing later values to the next cell. On the return journey it passes the next cell's reversed output before emitting its own retained value. This turns the chain into a distributed LIFO stack.

Here is one cell template. Its ports $l,r$ carry incoming values towards the tail; $v,u$ carry returning values towards the front. Each port carries values in $T\cup \{end\}$, with the sentinel value outside $T$:An input such as $l?x:T$ abbreviates an indexed CSP external choice over the corresponding CSP events. An output $r!y$ is the CSP prefixing action $r.y$. There is no extra controller process.

For $n\ge 1$, take $n$ copies of this same template. Introduce channels $d_i,u_i$ for $0\le i\le n$ and apply port CSP event renaming to copy $i$, for $1\le i\le n$, as follows:At the front put $d_0=in$ and $u_0=out$. Adjacent cells synchronize on every shared $d_i$ or $u_i$ CSP event. The two tail channels $d_n,u_n$ are sentinel-only: $d_n.end$ and $u_n.end$ are local tail CSP events, with no other participant required. Disable all $d_n.x,u_n.x$ for $x\in T$. Formally, use a partial relational CSP event renaming for the last copy, omitting the pairs for its $r.x,v.x$ with $x\in T$; an unmapped transition is blocked. This explicitly prevents a fictitious tail from generating data.

Let $C_i$ be the resulting port-renamed cell and $A_i$ its visible alphabet. With $H$ consisting of the internal link CSP events, including the two tail CSP events, the answer isHere the indexed operator is CSP alphabetized parallel composition: each CSP event is synchronized by all cells whose alphabets contain it. There are exactly $n$ storage-cell processes; port wiring and the sentinel-only tail adapt their interfaces, without adding a helper process. The local tail CSP events are hidden, as are all inter-cell communications.

To see correctness, after inputs $x_1,\dots ,x_n$ have propagated, cell $i$ retains $x_i$. The input sentinel value propagates to the tail. The last cell performs its two local tail CSP events, then returns $x_n,end$. Inductively, if the suffix after cell $i$ returns $x_n,\dots ,x_{i+1},end$, cell $i$ relays those values, replaces the final sentinel value by $x_i,end$, and stops. Hence the external output isand starts only after $in.end$. Shared links provide synchronization rather than an assumption that all cells take steps simultaneously. For the degenerate known-empty input, no storage is needed: the interface is simply $in.end\to out.end\to \mathrm{STOP}$.

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.Write $L_h$ for the resulting sequence of nodes at level $h$. The abstraction function isIt preserves repetitions, because distinct nodes may carry equal values. A suitable representation invariant requires the following:

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.