/* Tatica isolateln */

\tbegin
\ttactic isolateIn()  \def

\tappliesto ((AC \circseq Ao) \lpar ns1 | \lchanset cs \rchanset  | ns2 \rpar Ast)

        \tdo
            (\tskip \parallelbox \tlaw Sequence_Unit_part_1())  \tsemi 
			\tlaw Parallel_Composition_Sequence_step() \tsemi
            (\tskip \semibox (\tlaw Parallel_composition_commutativity() \tsemi 
			/*	((\tlaw copy_rule \semibox \tskip) \semibox \tskip) */
		\tlaw Schemas_Parallelism_composition_distribution() 
			\tsemi (\tskip \semibox \tlaw Parallel_composition_commutativity()))) \tsemi 
            \tlaw Sequence_Associativity()
			
\tend