Unique fixed point principle (source code)

= Unique fixed point principle
{title2=$P=F(P),\ Q=F(Q)\Rightarrow P=Q$}

For a suitably <guarded recursion>, two solutions of the same defining equation denote the same <CSP process>. There is also a mutually recursive version, comparing tuples of solutions.