		Search-engine friendly clone of the ACL2 documentation.

Pfcs

Well-formedness

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.

Subtopics

Definition-list-wfp: Check if a list of definitions is well-formed.
Definition-wfp: Check if a definition is well-formed.
Constraint-wfp: Check if a constraint is well-formed, with respect to a list of relation definitions.
Constraint-list-wfp: Check if a list of constraints is well-formed, with respect to a list of relation definitions.
System-wfp: Check if a system is well-formed.