\begin{circuslaw}{distr-rec-par-2}
\begin{circusaction*}
  \circmu X \circspot (((c_1 \then A_1 \extchoice c_2 \then A_2) \circseq A_3) \lpar ns_1 | cs | ns_2 \rpar (c_1 \then A_4)) \circseq X \; \equiv
  \also
  (\circmu X \circspot (c_1 \then A_1 \extchoice c_2 \then A_2) \circseq A_3 \circseq X) \lpar ns_1 | cs | ns_2 \rpar (\circmu X \circspot c_1 \then A_4 \then X)
  \also
  \provided \; \{c_1, c_2\} \subseteq cs \; \provand \; c_1 \notin \usedC(A_i) \; \mbox{for all} \; i \in \{1, 2, 3, 4\} \; \provand
  \also
  (\wrt(A_1) \cup \wrt(A_2) \cup \wrt(A_3)) \cap \used(A_4) = \emptyset \; \provand
  \also
  \wrt(A_4) \cap (\used(A_1) \cup \used(A_2) \cup \used(A_3)) = \emptyset
\end{circusaction*}
\end{circuslaw}
