(svar-boolmasks-limit-to-bound-vars keys boolvars) → xx
Function:
(defun svar-boolmasks-limit-to-bound-vars (keys boolvars) (declare (xargs :guard (and (svarlist-p keys) (svar-boolmasks-p boolvars)))) (let ((__function__ 'svar-boolmasks-limit-to-bound-vars)) (declare (ignorable __function__)) (if (atom keys) nil (let* ((look (svar-boolmasks-lookup (car keys) boolvars))) (cons (cons (svar-fix (car keys)) look) (svar-boolmasks-limit-to-bound-vars (cdr keys) boolvars))))))
Theorem:
(defthm svar-boolmasks-p-of-svar-boolmasks-limit-to-bound-vars (b* ((xx (svar-boolmasks-limit-to-bound-vars keys boolvars))) (svar-boolmasks-p xx)) :rule-classes :rewrite)
Theorem:
(defthm svar-boolmasks-limit-to-bound-vars-of-svarlist-fix-keys (equal (svar-boolmasks-limit-to-bound-vars (svarlist-fix keys) boolvars) (svar-boolmasks-limit-to-bound-vars keys boolvars)))
Theorem:
(defthm svar-boolmasks-limit-to-bound-vars-svarlist-equiv-congruence-on-keys (implies (svarlist-equiv keys keys-equiv) (equal (svar-boolmasks-limit-to-bound-vars keys boolvars) (svar-boolmasks-limit-to-bound-vars keys-equiv boolvars))) :rule-classes :congruence)
Theorem:
(defthm svar-boolmasks-limit-to-bound-vars-of-svar-boolmasks-fix-boolvars (equal (svar-boolmasks-limit-to-bound-vars keys (svar-boolmasks-fix boolvars)) (svar-boolmasks-limit-to-bound-vars keys boolvars)))
Theorem:
(defthm svar-boolmasks-limit-to-bound-vars-svar-boolmasks-equiv-congruence-on-boolvars (implies (svar-boolmasks-equiv boolvars boolvars-equiv) (equal (svar-boolmasks-limit-to-bound-vars keys boolvars) (svar-boolmasks-limit-to-bound-vars keys boolvars-equiv))) :rule-classes :congruence)