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