Juliano Cardoso / circusRefine

taticaIsolateSeqActions.tex 523 Bytes
edit raw blame history 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
/* Tatica isolateSeqActions */

\tbegin
\ttactic isolateSeqActions()  \def

\tappliesto ((AC0 \circseq A0) \lpar ns1 | \lchanset cs \rchanset  | ns2 \rpar (AC1 \circseq AO1)) 

        \tdo
            \tlaw Parallel_Composition_Sequence_step()  \tsemi 
            (\tskip \semibox\ (\tlaw Parallel_composition_commutativity() \tsemi \tlaw Parallel_Composition_Sequence_step() 
			\tsemi (\tskip \semibox\ \tlaw Parallel_composition_commutativity()))) \tsemi 
            \tlaw Sequence_Associativity()

\tend