\tbegin
\ttactic expDisjVarPar() \def
 
	 \tappliesto ((\circvar d0 : \nat \circspot A0) \lpar ns1 | cs | ns2 \rpar (\circvar d1 : \nat \circspot A1) )
      \tdo
		\tlaw var_exp_par() \tsemi \varbox (\tlaw  Parallel_composition_commutativity() \tsemi \tlaw var_exp_par() \tsemi 
		\varbox \tlaw Parallel_composition_commutativity()) 
		\tsemi \tlaw join_blocks() 
	\tend