Merge and termination in process algebra

In Vrancken (1986), the empty process epsilon was added to the algebra of communicating processes of Bergstra and Klop (1984, 1986). Reconsidering the definition of the parallel composition operator merge, the authors found that is preferable to explicitly state the termination option. This gives an extra summand in the defining equation of merge, using the auxiliary operator square root (tick). They find that tick can be defined in terms of the encapsulation operator delta /sub H/ and give an operational and a denotational semantics for the resulting system ACP square root , and prove that they are equal. The authors consider the limit rule, and prove it holds in the model