Errata for "Automating Open Bisimulation Checking for the Spi-Calculus (A. Tiu and J. Dawson, CSF 2010)"
In Definition 48, the reduction rules apply only to well-formed consistency
constraints whose theory components are consistent (the latter condition is missing
in the conference proceedings).
The point of the reduction is to show validity of the original constraint,
so there is no point in applying the rules further if the theory component is already inconsistent
in the original constraint.