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

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

\begin{circusaction}
	\circspot
		a.5.6?x \then \Skip
\end{circusaction}

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

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

\begin{circusaction}
	\circspot
		a.5.6!3 \then \Skip
\end{circusaction}

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

\begin{circus}
	\circprocess NotMS \circdef P1 \lpar \lchanset a \rchanset \rpar P2
\end{circus}
