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

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

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

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

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

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

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

\begin{circus}
	\circprocess R \circdef P \lpar \lchanset a \rchanset \rpar Q
\end{circus}