\begin{circus}
\circchannel chosenNumber : \nat
\end{circus}

\begin{circus}
\circchannel terminate, error
\end{circus}

\begin{circus}
\circprocess P \circdef \circbegin \\
	\circstate\ STATE ~~==~~ [~ x, n1, n2, n3, n4, n5, n6 : \nat ~] \\
	\circspot \Skip \\%chosenNumber.4 \then \Skip \\
	\circend
\end{circus}
