(sv::svarlist-masked-x-subst sv::vars sv::masks) → subst
Function:
(defun sv::svarlist-masked-x-subst (sv::vars sv::masks) (declare (xargs :guard (and (sv::svarlist-p sv::vars) (sv::4vmask-alist-p sv::masks)))) (let ((__function__ 'sv::svarlist-masked-x-subst)) (declare (ignorable __function__)) (b* (((when (atom sv::vars)) nil) (sv::var (sv::svar-fix (car sv::vars))) (sv::mask (cdr (hons-get sv::var (sv::4vmask-alist-fix sv::masks)))) ((when (or (not sv::mask) (bitops::sparseint-equal sv::mask 0))) (sv::svarlist-masked-x-subst (cdr sv::vars) sv::masks))) (cons (cons sv::var (sv::make-svex-call :fn 'sv::bit? :args (list (sv::svex-quote (sv::2vec (bitops::sparseint-val sv::mask))) (sv::svex-x) (sv::svex-var sv::var)))) (sv::svarlist-masked-x-subst (cdr sv::vars) sv::masks)))))
Theorem:
(defthm sv::svex-alist-p-of-svarlist-masked-x-subst (b* ((subst (sv::svarlist-masked-x-subst sv::vars sv::masks))) (sv::svex-alist-p subst)) :rule-classes :rewrite)
Theorem:
(defthm sv::vars-of-svarlist-masked-x-subst (b* ((common-lisp::?subst (sv::svarlist-masked-x-subst sv::vars sv::masks))) (implies (not (member-equal sv::v (sv::svarlist-fix sv::vars))) (not (member-equal sv::v (sv::svex-alist-vars subst))))))
Theorem:
(defthm sv::svarlist-masked-x-subst-of-svarlist-fix-vars (equal (sv::svarlist-masked-x-subst (sv::svarlist-fix sv::vars) sv::masks) (sv::svarlist-masked-x-subst sv::vars sv::masks)))
Theorem:
(defthm sv::svarlist-masked-x-subst-svarlist-equiv-congruence-on-vars (implies (sv::svarlist-equiv sv::vars sv::vars-equiv) (equal (sv::svarlist-masked-x-subst sv::vars sv::masks) (sv::svarlist-masked-x-subst sv::vars-equiv sv::masks))) :rule-classes :congruence)
Theorem:
(defthm sv::svarlist-masked-x-subst-of-4vmask-alist-fix-masks (equal (sv::svarlist-masked-x-subst sv::vars (sv::4vmask-alist-fix sv::masks)) (sv::svarlist-masked-x-subst sv::vars sv::masks)))
Theorem:
(defthm sv::svarlist-masked-x-subst-4vmask-alist-equiv-congruence-on-masks (implies (sv::4vmask-alist-equiv sv::masks sv::masks-equiv) (equal (sv::svarlist-masked-x-subst sv::vars sv::masks) (sv::svarlist-masked-x-subst sv::vars sv::masks-equiv))) :rule-classes :congruence)