\begin{circuslaw}{seq-op-comm}
\begin{circusaction*}
  A \circseq Op ~ \equiv ~ Op \circseq A
  \also
  \provided \used(Op) \cup \wrt(A) = \emptyset \; \provand \; \used(A) \cup \wrt(Op) = \emptyset
\end{circusaction*}
\end{circuslaw}
