(constraintlist-add-pathcond cond negatedp constraints) → new-constraints
Function:
(defun constraintlist-add-pathcond (cond negatedp constraints) (declare (xargs :guard (and (svex-p cond) (constraintlist-p constraints)))) (let ((__function__ 'constraintlist-add-pathcond)) (declare (ignorable __function__)) (if (atom constraints) nil (cons (change-constraint (car constraints) :cond (svcall bitor (if negatedp cond (svcall bitnot (svcall uor cond))) (constraint->cond (car constraints)))) (constraintlist-add-pathcond cond negatedp (cdr constraints))))))
Theorem:
(defthm constraintlist-p-of-constraintlist-add-pathcond (b* ((new-constraints (constraintlist-add-pathcond cond negatedp constraints))) (constraintlist-p new-constraints)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-constraintlist-add-pathcond (b* ((?new-constraints (constraintlist-add-pathcond cond negatedp constraints))) (implies (and (not (member v (constraintlist-vars constraints))) (not (member v (svex-vars cond)))) (not (member v (constraintlist-vars new-constraints))))))
Theorem:
(defthm constraintlist-add-pathcond-of-svex-fix-cond (equal (constraintlist-add-pathcond (svex-fix cond) negatedp constraints) (constraintlist-add-pathcond cond negatedp constraints)))
Theorem:
(defthm constraintlist-add-pathcond-svex-equiv-congruence-on-cond (implies (svex-equiv cond cond-equiv) (equal (constraintlist-add-pathcond cond negatedp constraints) (constraintlist-add-pathcond cond-equiv negatedp constraints))) :rule-classes :congruence)
Theorem:
(defthm constraintlist-add-pathcond-of-constraintlist-fix-constraints (equal (constraintlist-add-pathcond cond negatedp (constraintlist-fix constraints)) (constraintlist-add-pathcond cond negatedp constraints)))
Theorem:
(defthm constraintlist-add-pathcond-constraintlist-equiv-congruence-on-constraints (implies (constraintlist-equiv constraints constraints-equiv) (equal (constraintlist-add-pathcond cond negatedp constraints) (constraintlist-add-pathcond cond negatedp constraints-equiv))) :rule-classes :congruence)