\begin{circuslaw}{distr-prefix-par-5}
\begin{circusaction*}
  c~?~x \then v := x \circseq (A_1 \lpar ns_1 | cs | ns_2 \rpar A_2) \; \equiv
  \also
  (c~?~x \then v := x \circseq A_1) \lpar ns_1 \cup \{v\} | cs | ns_2 \rpar (c~?~\anyvar \then A_2)
  \also
  \provided ~ c \in cs \; \provand \; \mbox{$v$ and $y$ are not free in $A_2$}
\end{circusaction*}
\end{circuslaw}
