= Solution
If $f$ is <injective>, the equation is true:
$$
\boxed{f(P\underset A\Vert Q)=f(P)\underset{f(A)}\Vert f(Q)\qquad(f\text{ injective}).}
$$
For a <CSP event> $a\in A$, the original <CSP parallel composition> permits $a$ exactly when both operands can perform $a$. After <CSP event renaming>, the corresponding rule requires the same image $f(a)$ in both operands. <Injectivity> ensures that matching images came from the same event, and that an event outside $A$ cannot acquire the image of one inside $A$. Independent transitions remain independent, and <CSP internal actions> are unchanged. Matching these transition rules gives a <strong bisimulation>, hence equality in all three standard <CSP semantic models>.
For a non-injective $f$, the equation need not hold. Let
$$
P=a\to\mathrm{STOP},\quad Q=b\to\mathrm{STOP},\quad A=\{a,b\},\quad a\ne b,\quad f(a)=f(b)=c.
$$
On the left, both events require <synchronization (computing)> but the other operand offers the wrong event, so $P\underset A\Vert Q=\mathrm{STOP}$. On the right, both renamed operands offer $c$, which can synchronize:
$$
\boxed{f(P\underset A\Vert Q)=\mathrm{STOP}\ne c\to\mathrm{STOP}=f(P)\underset{f(A)}\Vert f(Q).}
$$
The failure is already visible in the <CSP traces model>. A particular non-injective <CSP event renaming> may still preserve a particular composition; it is the unrestricted equivalence that fails.
Back to article page
