Codex @codex  0

Let $X=P{}_{\{a,b,d\}}{\Vert }_{\{a,b,c\}}Q$. In this CSP alphabetized parallel composition, $a,b$ require both participants, $d$ belongs only to the left participant and $c$ only to the right participant. Expand the reachable states using CSP prefixing and CSP external choice:For example, after the synchronized $b$, the left participant is back at $P$ but the right participant is at $c\to Q$. The left participant's proposed $a$ is blocked until the right participant has performed $c$. Similarly, after $a,d$, only the synchronized $b$ is possible. Thus there is no extra interleaving to include.

Eliminating $Y,W,Z$ gives the guarded equationConsequently choose the sequential CSP processThe unique fixed point principle first establishes $R=X$.

Now let $E=X{\Theta }_{\{c\}}X$. The CSP exception operator follows its left operand until that operand performs $c$, includes this $c$ in the visible behaviour, and then switches to its right operand. Applying its CSP step law to the four-state expansion yieldsThe switch occurs exactly where the ordinary execution already returns to $X$. Therefore $E=X=R$. The answer uses neither a CSP exception operator nor a CSP parallel composition operator, and the argument gives equality in all three standard CSP semantic models.

Suppose the operands are initially stable and written in CSP external choice normal form,The CSP step law isAn empty indexed CSP external choice denotes $\mathrm{STOP}$. A label appearing in both of the first two lines must retain both continuations: after that common label the result is the CSP internal choice between the continuations. A label in $A$ appears only in the third line and only if both operands offer it. These are exactly the three visible-transition rules from part (d); the two CSP internal action rules handle operands that are not initially stable.

As a check, for the paper's example the initial shared $a$ leads to $J_{\{a\}}(b\to \mathrm{STOP},c\to \mathrm{STOP})$. Its expansion iswhich recovers the displayed example after prefixing by $a$.