\begin{circuslaw}{distr-rec-par-1}
\begin{circusaction*}
  \circmu X \circspot (A_1 \lpar ns_1 | cs | ns_2 \rpar A_2) \circseq c \then X \; \equiv \;
  \also
  (\circmu X \circspot A_1 \circseq c \then X) \lpar ns_1 | cs | ns_2 \rpar (\circmu X \circspot A_2 \circseq c \then X)
  \also
  \provided c \in cs \; \provand \; c \notin \usedC(A_1) \cup \usedC(A_2) \; \provand
  \also
  \wrt(A_1) \cap \used(A_2) = \emptyset \; \provand \; \wrt(A_2) \cap \used(A_1)
\end{circusaction*}
\end{circuslaw}
