/* Tactic: BjSt4D_config2*/

\tbegin
\ttactic BjSt4D_config2()  \def

 /*\tappliesto  ((((in1 inter x \then ((st1:=x \circseq A1) \circseq A2)) \circseq A3) \linter ns1 | ns2 \rinter (in2 inter x \circthen st2:=x)) \circseq A4 )*/

/*  \tdo */
(((((( \thenbox \tlaw Sequence_Associativity() \tsemi \tlaw Prefix_Sequential_Composition_Associativity()) \semibox \tskip)
       \tsemi \tlaw Sequence_Associativity()) \interleavebox \tskip) 
	   \tsemi \tlaw inter_seq_extratc_snd()
	   \tsemi (( \tlaw Inter_unused_name(st2) \tsemi \tlaw inter_comm()
                \tsemi \tlaw Inter_Unused_Name(st1) \tsemi \tlaw inter_comm())  \semibox \tskip)
				\semibox \tskip))
\tsemi \tlaw Sequence_Associativity()

\tend