		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Constraint-rels

Set of (names of) relations in a constraint.

Signature
(constraint-rels constr) → rels
Arguments: constr — Guard (constraintp constr).
Returns: rels — Type (string-setp rels).

This is the empty set for an equality constraint; for a relation constraint, it is the singleton with that constraint relation. This function is used to define constraint-list-rels.

Definitions and Theorems

Function: constraint-rels

(defun constraint-rels (constr)
  (declare (xargs :guard (constraintp constr)))
  (let ((__function__ 'constraint-rels))
    (declare (ignorable __function__))
    (constraint-case constr
                     :equal nil
                     :relation (insert constr.name nil))))

Theorem: string-setp-of-constraint-rels

(defthm string-setp-of-constraint-rels
  (b* ((rels (constraint-rels constr)))
    (string-setp rels))
  :rule-classes :rewrite)

Theorem: constraint-rels-of-constraint-fix-constr

(defthm constraint-rels-of-constraint-fix-constr
  (equal (constraint-rels (constraint-fix constr))
         (constraint-rels constr)))

Theorem: constraint-rels-constraint-equiv-congruence-on-constr

(defthm constraint-rels-constraint-equiv-congruence-on-constr
  (implies (constraint-equiv constr constr-equiv)
           (equal (constraint-rels constr)
                  (constraint-rels constr-equiv)))
  :rule-classes :congruence)