On Bisimilarity and Substitution in Presence of Replication
We prove a new congruence result for the -calculus: bisim- ilarity is a congruence in the sub-calculus that does not include restric- tion nor sum, and features top-level replications. Our proof relies on algebraic properties of replication, and on a new syntactic characteri- sation of bisimilarity. We obtain this characterisation using a rewriting system rather than a purely equational axiomatisation. We then deduce substitution closure, and hence, congruence. Whether bisimilarity is a congruence when replications are unrestricted remains open.