(constraintlist-subst-from-svexarr x aliases svexarr) → xx
Function:
(defun constraintlist-subst-from-svexarr (x aliases svexarr) (declare (xargs :stobjs (aliases svexarr))) (declare (xargs :guard (constraintlist-p x))) (declare (xargs :guard (and (svarlist-boundedp (constraintlist-vars x) (aliass-length aliases)) (svarlist-boundedp (constraintlist-vars x) (svexs-length svexarr))))) (let ((__function__ 'constraintlist-subst-from-svexarr)) (declare (ignorable __function__)) (mbe :logic (b* (((when (atom x)) nil) ((constraint x1) (car x)) (cond (svex-subst-from-svexarr x1.cond svexarr))) (cons (change-constraint x1 :cond cond) (constraintlist-subst-from-svexarr (cdr x) aliases svexarr))) :exec (if (atom x) nil (with-local-stobj nrev (mv-let (ans nrev) (b* ((nrev (constraintlist-subst-from-svexarr-nrev x aliases svexarr nrev)) ((mv ans nrev) (acl2::nrev-finish nrev))) (mv ans nrev)) ans))))))
Theorem:
(defthm constraintlist-p-of-constraintlist-subst-from-svexarr (b* ((xx (constraintlist-subst-from-svexarr x aliases svexarr))) (constraintlist-p xx)) :rule-classes :rewrite)
Theorem:
(defthm constraintlist-subst-from-svexarr-of-constraintlist-fix-x (equal (constraintlist-subst-from-svexarr (constraintlist-fix x) aliases svexarr) (constraintlist-subst-from-svexarr x aliases svexarr)))
Theorem:
(defthm constraintlist-subst-from-svexarr-constraintlist-equiv-congruence-on-x (implies (constraintlist-equiv x x-equiv) (equal (constraintlist-subst-from-svexarr x aliases svexarr) (constraintlist-subst-from-svexarr x-equiv aliases svexarr))) :rule-classes :congruence)
Theorem:
(defthm constraintlist-subst-from-svexarr-of-lhslist-fix-aliases (equal (constraintlist-subst-from-svexarr x (lhslist-fix aliases) svexarr) (constraintlist-subst-from-svexarr x aliases svexarr)))
Theorem:
(defthm constraintlist-subst-from-svexarr-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (constraintlist-subst-from-svexarr x aliases svexarr) (constraintlist-subst-from-svexarr x aliases-equiv svexarr))) :rule-classes :congruence)
Theorem:
(defthm svarlist-addr-p-of-constraintlist-subst-from-svexarr (implies (and (svarlist-addr-p (svexarr-vars svexarr)) (svarlist-addr-p (aliases-vars aliases))) (svarlist-addr-p (constraintlist-vars (constraintlist-subst-from-svexarr x aliases svexarr)))))