(svtv-inalist-resolve-unassigned inalist masks phase) → inalist1
Function:
(defun svtv-inalist-resolve-unassigned (inalist masks phase) (declare (xargs :guard (and (svex-alist-p inalist) (4vmask-alist-p masks) (natp phase)))) (let ((__function__ 'svtv-inalist-resolve-unassigned)) (declare (ignorable __function__)) (b* ((inalist (svex-alist-fix inalist)) (masks (4vmask-alist-fix masks)) ((when (atom inalist)) nil) ((cons var expr) (car inalist)) (mask (or (cdr (hons-get var masks)) 0)) (exp (svex-call 'bit? (list (svex-quote (2vec (sparseint-val mask))) expr (svex-var (svex-phase-var var phase)))))) (cons (cons var exp) (svtv-inalist-resolve-unassigned (cdr inalist) masks phase)))))
Theorem:
(defthm svex-alist-p-of-svtv-inalist-resolve-unassigned (b* ((inalist1 (svtv-inalist-resolve-unassigned inalist masks phase))) (svex-alist-p inalist1)) :rule-classes :rewrite)
Theorem:
(defthm svtv-inalist-resolve-unassigned-of-svex-alist-fix-inalist (equal (svtv-inalist-resolve-unassigned (svex-alist-fix inalist) masks phase) (svtv-inalist-resolve-unassigned inalist masks phase)))
Theorem:
(defthm svtv-inalist-resolve-unassigned-svex-alist-equiv-congruence-on-inalist (implies (svex-alist-equiv inalist inalist-equiv) (equal (svtv-inalist-resolve-unassigned inalist masks phase) (svtv-inalist-resolve-unassigned inalist-equiv masks phase))) :rule-classes :congruence)
Theorem:
(defthm svtv-inalist-resolve-unassigned-of-4vmask-alist-fix-masks (equal (svtv-inalist-resolve-unassigned inalist (4vmask-alist-fix masks) phase) (svtv-inalist-resolve-unassigned inalist masks phase)))
Theorem:
(defthm svtv-inalist-resolve-unassigned-4vmask-alist-equiv-congruence-on-masks (implies (4vmask-alist-equiv masks masks-equiv) (equal (svtv-inalist-resolve-unassigned inalist masks phase) (svtv-inalist-resolve-unassigned inalist masks-equiv phase))) :rule-classes :congruence)
Theorem:
(defthm svtv-inalist-resolve-unassigned-of-nfix-phase (equal (svtv-inalist-resolve-unassigned inalist masks (nfix phase)) (svtv-inalist-resolve-unassigned inalist masks phase)))
Theorem:
(defthm svtv-inalist-resolve-unassigned-nat-equiv-congruence-on-phase (implies (nat-equiv phase phase-equiv) (equal (svtv-inalist-resolve-unassigned inalist masks phase) (svtv-inalist-resolve-unassigned inalist masks phase-equiv))) :rule-classes :congruence)