		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Constraintlist-compose

Signature
(constraintlist-compose x a) → new-x
Arguments: x — Guard (constraintlist-p x).; a — Guard (svex-alist-p a).
Returns: new-x — Type (constraintlist-p new-x).

Definitions and Theorems

Function: constraintlist-compose

(defun constraintlist-compose (x a)
  (declare (xargs :guard (and (constraintlist-p x)
                              (svex-alist-p a))))
  (let ((__function__ 'constraintlist-compose))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (change-constraint
                 (car x)
                 :cond (svex-compose (constraint->cond (car x))
                                     a))
            (constraintlist-compose (cdr x) a)))))

Theorem: constraintlist-p-of-constraintlist-compose

(defthm constraintlist-p-of-constraintlist-compose
  (b* ((new-x (constraintlist-compose x a)))
    (constraintlist-p new-x))
  :rule-classes :rewrite)

Theorem: vars-of-constraintlist-compose

(defthm vars-of-constraintlist-compose
  (b* ((?new-x (constraintlist-compose x a)))
    (implies (and (not (member v (constraintlist-vars x)))
                  (not (member v (svex-alist-vars a))))
             (not (member v (constraintlist-vars new-x))))))

Theorem: constraintlist-compose-of-constraintlist-fix-x

(defthm constraintlist-compose-of-constraintlist-fix-x
  (equal (constraintlist-compose (constraintlist-fix x)
                                 a)
         (constraintlist-compose x a)))

Theorem: constraintlist-compose-constraintlist-equiv-congruence-on-x

(defthm constraintlist-compose-constraintlist-equiv-congruence-on-x
  (implies (constraintlist-equiv x x-equiv)
           (equal (constraintlist-compose x a)
                  (constraintlist-compose x-equiv a)))
  :rule-classes :congruence)

Theorem: constraintlist-compose-of-svex-alist-fix-a

(defthm constraintlist-compose-of-svex-alist-fix-a
  (equal (constraintlist-compose x (svex-alist-fix a))
         (constraintlist-compose x a)))

Theorem: constraintlist-compose-svex-alist-equiv-congruence-on-a

(defthm constraintlist-compose-svex-alist-equiv-congruence-on-a
  (implies (svex-alist-equiv a a-equiv)
           (equal (constraintlist-compose x a)
                  (constraintlist-compose x a-equiv)))
  :rule-classes :congruence)