\begin{circus}
	\circchannel a, b, c: \nat
\end{circus}

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

\begin{circusaction}
	\circspot
		a.5 \then \Skip
\end{circusaction}

\begin{circus}	
	\circend
\end{circus}

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

\begin{circusaction}
	\circspot
		a.5 \then \Skip
\end{circusaction}

\begin{circus}	
	\circend
\end{circus}

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

\begin{circusaction}
	\circspot
		a.5 \then \Skip
\end{circusaction}

\begin{circus}	
	\circend
\end{circus}

\begin{circus}
	\circprocess P4 \circdef P1 \lpar \lchanset a \rchanset \rpar (P2 \lpar \lchanset b \rchanset \rpar P3) \end{circus}

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

\begin{circusaction}
	\circspot
		b!5 \then \Skip
\end{circusaction}

\begin{circus}	
	\circend
\end{circus}

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

\begin{circusaction}
	\circspot
		b?x \then \Skip
\end{circusaction}

\begin{circus}	
	\circend
\end{circus}

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

\begin{circusaction}
	\circspot
		b?x \then \Skip
\end{circusaction}

\begin{circus}	
	\circend
\end{circus}

\begin{circus}
	\circprocess P8 \circdef P5 \lpar \lchanset b \rchanset \rpar (P6 \lpar \lchanset a \rchanset \rpar P7) \end{circus}
