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

\begin{circus}
\circprocess Output \circdef \circbegin
\end{circus}

\begin{circusaction}
\circstate Stt ~~==~~ [~ cinco: \nat; seis : \nat \where cinco = 5 \land seis =
6 ~]
\end{circusaction}

\begin{circusaction}
	\circspot out.cinco \then \Skip
\end{circusaction}
\begin{circus}
	\circend
\end{circus}
