(vl-make-duperhs-alist-aux x alist) → new-alist
Function:
(defun vl-make-duperhs-alist-aux (x alist) (declare (xargs :guard (and (vl-assignlist-p x) (vl-duperhs-alist-p alist)))) (let ((__function__ 'vl-make-duperhs-alist-aux)) (declare (ignorable __function__)) (b* ((alist (vl-duperhs-alist-fix alist)) ((when (atom x)) alist) ((vl-assign x1) (vl-assign-fix (car x))) (rhs1 (hons-copy (vl-expr-strip x1.expr))) (look (hons-get rhs1 alist)) (alist (hons-acons rhs1 (cons x1 (cdr look)) alist))) (vl-make-duperhs-alist-aux (cdr x) alist))))
Theorem:
(defthm vl-duperhs-alist-p-of-vl-make-duperhs-alist-aux (b* ((new-alist (vl-make-duperhs-alist-aux x alist))) (vl-duperhs-alist-p new-alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-make-duperhs-alist-aux-of-vl-assignlist-fix-x (equal (vl-make-duperhs-alist-aux (vl-assignlist-fix x) alist) (vl-make-duperhs-alist-aux x alist)))
Theorem:
(defthm vl-make-duperhs-alist-aux-vl-assignlist-equiv-congruence-on-x (implies (vl-assignlist-equiv x x-equiv) (equal (vl-make-duperhs-alist-aux x alist) (vl-make-duperhs-alist-aux x-equiv alist))) :rule-classes :congruence)
Theorem:
(defthm vl-make-duperhs-alist-aux-of-vl-duperhs-alist-fix-alist (equal (vl-make-duperhs-alist-aux x (vl-duperhs-alist-fix alist)) (vl-make-duperhs-alist-aux x alist)))
Theorem:
(defthm vl-make-duperhs-alist-aux-vl-duperhs-alist-equiv-congruence-on-alist (implies (vl-duperhs-alist-equiv alist alist-equiv) (equal (vl-make-duperhs-alist-aux x alist) (vl-make-duperhs-alist-aux x alist-equiv))) :rule-classes :congruence)