Solution (source code)

= Solution

Take a fresh <CSP event> $h$ and define
$$
\boxed{P=(h\to P)\setminus\{h\}.}
$$
The apparent guard is removed by <CSP hiding>. Each unfolding can perform a <CSP internal action> and return to the same situation without any visible <CSP event>. Operationally this is an infinite internal loop, a <CSP divergence>, so the equation is not a <guarded recursion>. This is precisely why a syntactic test that counts every occurrence of $\to$ would be wrong.