\begin{circuslaw}{lockstep-intro}
\begin{circusaction*}
  (\circmu X \circspot (A_1 \lpar ns_1 | cs | ns_2 \rpar A_2) \circseq X) ~ \equiv
  \also
  \t1
  \circblockopen
    (\circmu X \circspot A_1 \circseq sync \then X)
    \\
    \t1 \lpar ns_1 | cs \cup \lchanset Sync \rchanset | ns_2 \rpar
    \\
    (\circmu X \circspot A_2 \circseq sync \then X)
  \circblockclose
  \circhide \lchanset sync \rchanset
  \also
  \provided \; sync \notin \usedC(A_1) \cup \usedC(A_2) \; \provand \; \wrt(A_1) \cap \used(A_2) = \emptyset \; \provand
  \also
  \wrt(A_2) \cap \used(A_1) = \emptyset
\end{circusaction*}
\end{circuslaw}
