/* Tatica isolateSeqActions */

\tbegin
\ttactic isolateSeqActions()  \def

\tappliesto\ ((AC0 \circseq A_O_0) \lpar ns_1 | \lchanset cs \rchanset  | ns_2 \rpar (A_C_1 \circseq A_O_1)) 

        \tdo
            \tlaw Parallel_Composition_Sequence_step()  \tsemi 
            (\tskip \semibox\ (\tlaw Parallel_composition_commutativity() \tsemi \tlaw Parallel_Composition_Sequence_step() 
			\tsemi (\tskip \semibox\ \tlaw Parallel_composition_commutativity()))) \tsemi 
            \tlaw Sequence_Associativity()

\tend