(sv::4vmask-alist-unset-nonblocking acl2::x) → sv::new-x
Function:
(defun sv::4vmask-alist-unset-nonblocking (acl2::x) (declare (xargs :guard (sv::4vmask-alist-p acl2::x))) (let ((__function__ 'sv::4vmask-alist-unset-nonblocking)) (declare (ignorable __function__)) (b* ((acl2::x (sv::4vmask-alist-fix acl2::x))) (if (atom acl2::x) nil (cons (cons (sv::change-svar (caar acl2::x) :bits (logandc1 256 (sv::svar->bits (caar acl2::x)))) (cdar acl2::x)) (sv::4vmask-alist-unset-nonblocking (cdr acl2::x)))))))
Theorem:
(defthm sv::4vmask-alist-p-of-4vmask-alist-unset-nonblocking (b* ((sv::new-x (sv::4vmask-alist-unset-nonblocking acl2::x))) (sv::4vmask-alist-p sv::new-x)) :rule-classes :rewrite)
Theorem:
(defthm sv::4vmask-alist-unset-nonblocking-of-4vmask-alist-fix-x (equal (sv::4vmask-alist-unset-nonblocking (sv::4vmask-alist-fix acl2::x)) (sv::4vmask-alist-unset-nonblocking acl2::x)))
Theorem:
(defthm sv::4vmask-alist-unset-nonblocking-4vmask-alist-equiv-congruence-on-x (implies (sv::4vmask-alist-equiv acl2::x sv::x-equiv) (equal (sv::4vmask-alist-unset-nonblocking acl2::x) (sv::4vmask-alist-unset-nonblocking sv::x-equiv))) :rule-classes :congruence)