(svexlist-compute-masks x mask-al) → mask-al1
Function:
(defun svexlist-compute-masks (x mask-al) (declare (xargs :guard (and (svexlist-p x) (svex-mask-alist-p mask-al)))) (let ((__function__ 'svexlist-compute-masks)) (declare (ignorable __function__)) (b* (((when (atom x)) (mbe :logic (svex-mask-alist-fix mask-al) :exec mask-al)) (first (car x)) ((when (not (eq (svex-kind first) :call))) (svexlist-compute-masks (cdr x) mask-al)) (mask (svex-mask-lookup first mask-al)) ((when (sparseint-equal mask 0)) (svexlist-compute-masks (cdr x) mask-al)) (args (svex-call->args first)) (argmasks (svex-argmasks mask (svex-call->fn first) args)) (mask-al (svex-args-apply-masks args argmasks mask-al))) (svexlist-compute-masks (cdr x) mask-al))))
Theorem:
(defthm svex-mask-alist-p-of-svexlist-compute-masks (b* ((mask-al1 (svexlist-compute-masks x mask-al))) (svex-mask-alist-p mask-al1)) :rule-classes :rewrite)
Theorem:
(defthm svexlist-compute-masks-lookup-subsumes-prev-lookup (4vmask-subsumes (svex-mask-lookup y (svexlist-compute-masks x mask-al)) (svex-mask-lookup y mask-al)))
Theorem:
(defthm svexlist-compute-masks-lookup-when-all (implies (sparseint-equal (svex-mask-lookup y mask-al) -1) (sparseint-equal (svex-mask-lookup y (svexlist-compute-masks x mask-al)) -1)))
Theorem:
(defthm svexlist-compute-masks-lookup-when-neg1 (implies (equal (svex-mask-lookup y mask-al) -1) (equal (svex-mask-lookup y (svexlist-compute-masks x mask-al)) -1)))
Theorem:
(defthm svexlist-compute-masks-lookups-subsume-prev-lookups (4vmasklist-subsumes (svex-argmasks-lookup y (svexlist-compute-masks x mask-al)) (svex-argmasks-lookup y mask-al)))
Theorem:
(defthm svexlist-compute-masks-partly-complete (implies (and (svex-mask-alist-partly-complete x mask-al) (svexlist-toposort-p x)) (svex-mask-alist-partly-complete nil (svexlist-compute-masks x mask-al))))
Theorem:
(defthm svexlist-compute-masks-of-svexlist-fix-x (equal (svexlist-compute-masks (svexlist-fix x) mask-al) (svexlist-compute-masks x mask-al)))
Theorem:
(defthm svexlist-compute-masks-svexlist-equiv-congruence-on-x (implies (svexlist-equiv x x-equiv) (equal (svexlist-compute-masks x mask-al) (svexlist-compute-masks x-equiv mask-al))) :rule-classes :congruence)
Theorem:
(defthm svexlist-compute-masks-of-svex-mask-alist-fix-mask-al (equal (svexlist-compute-masks x (svex-mask-alist-fix mask-al)) (svexlist-compute-masks x mask-al)))
Theorem:
(defthm svexlist-compute-masks-svex-mask-alist-equiv-congruence-on-mask-al (implies (svex-mask-alist-equiv mask-al mask-al-equiv) (equal (svexlist-compute-masks x mask-al) (svexlist-compute-masks x mask-al-equiv))) :rule-classes :congruence)