(combine-mask-alists masks acc) → res
Function:
(defun combine-mask-alists (masks acc) (declare (xargs :guard (and (sv::4vmask-alist-p masks) (sv::4vmask-alist-p acc)))) (let ((__function__ 'combine-mask-alists)) (declare (ignorable __function__)) (b* ((masks (sv::4vmask-alist-fix masks)) (acc (sv::4vmask-alist-fix acc)) ((when (atom masks)) acc) ((cons key val) (car masks)) (look (or (cdr (hons-get key acc)) 0)) (newval (bitops::sparseint-bitor val look))) (combine-mask-alists (cdr masks) (hons-acons key newval acc)))))
Theorem:
(defthm 4vmask-alist-p-of-combine-mask-alists (b* ((res (combine-mask-alists masks acc))) (sv::4vmask-alist-p res)) :rule-classes :rewrite)
Theorem:
(defthm combine-mask-alists-of-4vmask-alist-fix-masks (equal (combine-mask-alists (sv::4vmask-alist-fix masks) acc) (combine-mask-alists masks acc)))
Theorem:
(defthm combine-mask-alists-4vmask-alist-equiv-congruence-on-masks (implies (sv::4vmask-alist-equiv masks masks-equiv) (equal (combine-mask-alists masks acc) (combine-mask-alists masks-equiv acc))) :rule-classes :congruence)
Theorem:
(defthm combine-mask-alists-of-4vmask-alist-fix-acc (equal (combine-mask-alists masks (sv::4vmask-alist-fix acc)) (combine-mask-alists masks acc)))
Theorem:
(defthm combine-mask-alists-4vmask-alist-equiv-congruence-on-acc (implies (sv::4vmask-alist-equiv acc acc-equiv) (equal (combine-mask-alists masks acc) (combine-mask-alists masks acc-equiv))) :rule-classes :congruence)