Well-formedness of PFCSes.
A constraint that is not an equality, i.e. that is an application of a named relation to some expressions, must reference a defined relation, and the number of argument expressions must match the number of parameters of the named relation. No two distinct relations may have the same name. The parameters of a named relation definition must be unique.
All these well-formedness conditions are formalized here.