\begin{circuslaw}{replace-sync-chan-seq}
\begin{circusaction*}
  \circblockopen
    (\circmu X \circspot A_1 \circseq c~!~x \then \Skip \circseq sync \then X)
    \also
    \t1 \lpar ns_1 | cs | ns_2 \rpar
    \also
    (\circmu X \circspot c~?~x \then A_2 \circseq sync \then X)
  \circblockclose
  \circhide \lchanset c \rchanset
  \also
  \t1 \equiv
  \also
  \circblockopen
    \circblockopen
      (\circmu X \circspot A_1 \circseq c_1~!~x \then \Skip \circseq sync \then X)
      \also
      \t1 \lpar ns_1 | cs \setdiff \lchanset c \rchanset | ns_2 \rpar
      \also
      (\circmu X \circspot c_2~?~x \then A_2 \circseq sync \then X)
    \circblockclose
    \also
    \t1 \lpar ns_1 \cup ns_2 | \lchanset c_1, c_2, sync \rchanset | \emptyset \rpar
    \also
    \circblockopen
      \circmu X \circspot c_1~?~x \then c_2~!~x \then \Skip \circseq sync \then X
    \circblockclose
  \circblockclose
  \circhide \lchanset c_1, c_2 \rchanset
  \also
  \provided ~ \lchanset c, sync \rchanset \subseteq cs \land c \notin \usedC(A_1) \cup \usedC(A_2) \; \provand \; \mbox{$c_1$ and $c_2$ are fresh channels}
\end{circusaction*}
\end{circuslaw}
