Extends vl-module-gate-elim across a module list.
(vl-modulelist-gate-elim-aux x primalist) → (mv new-x addmods)
Function:
(defun vl-modulelist-gate-elim-aux (x primalist) (declare (xargs :guard (and (vl-modulelist-p x) (vl-primalist-p primalist)))) (let ((__function__ 'vl-modulelist-gate-elim-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv car-prime car-addmods) (vl-module-gate-elim (car x) primalist)) ((mv cdr-prime cdr-addmods) (vl-modulelist-gate-elim-aux (cdr x) primalist))) (mv (cons car-prime cdr-prime) (append car-addmods cdr-addmods)))))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-gate-elim-aux.new-x (implies (and (force (vl-modulelist-p x)) (force (vl-primalist-p primalist))) (b* (((mv ?new-x ?addmods) (vl-modulelist-gate-elim-aux x primalist))) (vl-modulelist-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-gate-elim-aux.addmods (implies (and (force (vl-modulelist-p x)) (force (vl-primalist-p primalist))) (b* (((mv ?new-x ?addmods) (vl-modulelist-gate-elim-aux x primalist))) (vl-modulelist-p addmods))) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-gate-elim-aux-mvtypes-0 (true-listp (mv-nth 0 (vl-modulelist-gate-elim-aux x primalist))) :rule-classes :type-prescription)
Theorem:
(defthm vl-modulelist-gate-elim-aux-mvtypes-1 (true-listp (mv-nth 1 (vl-modulelist-gate-elim-aux x primalist))) :rule-classes :type-prescription)