= Solution
The <unique fixed point principle> says that a suitably <guarded recursion> has a unique solution in the chosen <CSP semantic model>. In particular, for a guarded process expression $F(X)$,
$$
\boxed{P=F(P),\quad Q=F(Q)\quad\Longrightarrow\quad P=Q.}
$$
The same principle applies to a mutually recursive system: two tuples satisfying the same guarded equations are componentwise equal. Thus an algebraic proof may show that a candidate satisfies the defining equations, instead of comparing arbitrarily long executions individually.
A <guarded recursion> must make visible progress before re-entering its recursive dependency. For an equation built from <CSP prefixing> and <CSP choice>, the usual sufficient condition is that every recursive occurrence lies behind a visible <CSP prefixing> operation. For mutually recursive equations, every dependency cycle must pass such a guard. The guard must survive enclosing operators: an event subsequently removed by <CSP hiding> does not provide visible progress. Equivalently, in the usual semantic formulation the recursion functional must be contractive in observable depth. Merely seeing an arrow somewhere before the variable is insufficient.
Back to article page
