(constraintlist-compose-svstack x a) → new-x
Function:
(defun constraintlist-compose-svstack (x a) (declare (xargs :guard (and (constraintlist-p x) (svstack-p a)))) (let ((__function__ 'constraintlist-compose-svstack)) (declare (ignorable __function__)) (if (atom x) nil (cons (change-constraint (car x) :cond (svex-compose-svstack (constraint->cond (car x)) a)) (constraintlist-compose-svstack (cdr x) a)))))
Theorem:
(defthm constraintlist-p-of-constraintlist-compose-svstack (b* ((new-x (constraintlist-compose-svstack x a))) (constraintlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-constraintlist-compose-svstack (b* ((?new-x (constraintlist-compose-svstack x a))) (implies (and (not (member v (constraintlist-vars x))) (not (member v (svex-alist-vars (svstack-to-svex-alist a))))) (not (member v (constraintlist-vars new-x))))))
Theorem:
(defthm constraintlist-compose-svstack-of-constraintlist-fix-x (equal (constraintlist-compose-svstack (constraintlist-fix x) a) (constraintlist-compose-svstack x a)))
Theorem:
(defthm constraintlist-compose-svstack-constraintlist-equiv-congruence-on-x (implies (constraintlist-equiv x x-equiv) (equal (constraintlist-compose-svstack x a) (constraintlist-compose-svstack x-equiv a))) :rule-classes :congruence)
Theorem:
(defthm constraintlist-compose-svstack-of-svstack-fix-a (equal (constraintlist-compose-svstack x (svstack-fix a)) (constraintlist-compose-svstack x a)))
Theorem:
(defthm constraintlist-compose-svstack-svstack-equiv-congruence-on-a (implies (svstack-equiv a a-equiv) (equal (constraintlist-compose-svstack x a) (constraintlist-compose-svstack x a-equiv))) :rule-classes :congruence)