		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Constraint-list-vars

Set of variables in a list of constraints.

Signature
(constraint-list-vars constrs) → vars
Arguments: constrs — Guard (constraint-listp constrs).
Returns: vars — Type (name-setp vars).

Definitions and Theorems

Function: constraint-list-vars

(defun constraint-list-vars (constrs)
  (declare (xargs :guard (constraint-listp constrs)))
  (let ((__function__ 'constraint-list-vars))
    (declare (ignorable __function__))
    (cond ((endp constrs) nil)
          (t (union (constraint-vars (car constrs))
                    (constraint-list-vars (cdr constrs)))))))

Theorem: name-setp-of-constraint-list-vars

(defthm name-setp-of-constraint-list-vars
  (b* ((vars (constraint-list-vars constrs)))
    (name-setp vars))
  :rule-classes :rewrite)

Theorem: constraint-list-vars-of-cons

(defthm constraint-list-vars-of-cons
  (equal (constraint-list-vars (cons constr constrs))
         (union (constraint-vars constr)
                (constraint-list-vars constrs))))

Theorem: constraint-list-vars-of-append

(defthm constraint-list-vars-of-append
  (equal (constraint-list-vars (append constrs1 constrs2))
         (union (constraint-list-vars constrs1)
                (constraint-list-vars constrs2))))

Theorem: constraint-list-vars-of-rev

(defthm constraint-list-vars-of-rev
  (equal (constraint-list-vars (rev constrs))
         (constraint-list-vars constrs)))