\tbegin
\ttactic expOutVarScope() \def
 
 \tappliesto\ (\circvar\ d : \nat \circspot A_In \circseq ((\circvar\ d_Out : \nat \circspot A_Out) \lpar ns_1 | cs | ns_2 \rpar A_St))

        \tdo
            \varbox
			((\tskip \semibox (\tlaw var_exp_par() \tsemi \tlaw Sequence_Unit_part_1())) 
			\tsemi \tlaw var_exp_seq() \tsemi 
                \varbox (\tskip \semibox \tlaw Sequence_Unit_Part_1() ))
       		\tsemi	 \tlaw join_blocks() 

			
			 \tend