		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Constraintlist-add-scope

Signature
(constraintlist-add-scope scope x) → new-x
Arguments: x — Guard (constraintlist-p x).
Returns: new-x — Type (constraintlist-p new-x).

Definitions and Theorems

Function: constraintlist-add-scope

(defun constraintlist-add-scope (scope x)
  (declare (xargs :guard (constraintlist-p x)))
  (let ((__function__ 'constraintlist-add-scope))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (change-constraint
                 (car x)
                 :name (cons scope (constraint->name (car x))))
            (constraintlist-add-scope scope (cdr x))))))

Theorem: constraintlist-p-of-constraintlist-add-scope

(defthm constraintlist-p-of-constraintlist-add-scope
  (b* ((new-x (constraintlist-add-scope scope x)))
    (constraintlist-p new-x))
  :rule-classes :rewrite)

Theorem: constraintlist-vars-of-constraintlist-add-scope

(defthm constraintlist-vars-of-constraintlist-add-scope
  (b* ((?new-x (constraintlist-add-scope scope x)))
    (equal (constraintlist-vars new-x)
           (constraintlist-vars x))))

Theorem: constraintlist-add-scope-of-constraintlist-fix-x

(defthm constraintlist-add-scope-of-constraintlist-fix-x
  (equal (constraintlist-add-scope scope (constraintlist-fix x))
         (constraintlist-add-scope scope x)))

Theorem: constraintlist-add-scope-constraintlist-equiv-congruence-on-x

(defthm
      constraintlist-add-scope-constraintlist-equiv-congruence-on-x
  (implies (constraintlist-equiv x x-equiv)
           (equal (constraintlist-add-scope scope x)
                  (constraintlist-add-scope scope x-equiv)))
  :rule-classes :congruence)