Juliano Cardoso / circusRefine

BJSt4A_config1.tex 456 Bytes
edit raw blame history 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
/* Tactic: BJSt4A_config1*/

\tbegin
\ttactic BJSt4A_config1()  \def

		\tlaw Parallel_Composition_Sequence_step() \tsemi
		((\tskip \semibox (\tskip \parallelbox (\tlaw Sequence_Associativity() \tsemi
		\tlaw Prefix_Sequential_Composition_Associativity()))
		\tsemi \ttactic interIntroAndSimpl()
		\tsemi \tlaw Prefix_Skip() 
		\tsemi (\tskip \semibox \tlaw Sequence_Associativity())
		\tsemi \tlaw Sequence_Associativity()))
    \tend