(vl-modulelist-weirdint-elim-aux x) → (mv new-x addmods)
Function:
(defun vl-modulelist-weirdint-elim-aux (x) (declare (xargs :guard (vl-modulelist-p x))) (let ((__function__ 'vl-modulelist-weirdint-elim-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv car-prime new1) (vl-module-weirdint-elim (car x))) ((mv cdr-prime new2) (vl-modulelist-weirdint-elim-aux (cdr x))) (x-prime (cons car-prime cdr-prime)) (new (append new1 new2))) (mv x-prime new))))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-weirdint-elim-aux.new-x (b* (((mv ?new-x ?addmods) (vl-modulelist-weirdint-elim-aux x))) (vl-modulelist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-weirdint-elim-aux.addmods (b* (((mv ?new-x ?addmods) (vl-modulelist-weirdint-elim-aux x))) (vl-modulelist-p addmods)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-weirdint-elim-aux-of-vl-modulelist-fix-x (equal (vl-modulelist-weirdint-elim-aux (vl-modulelist-fix x)) (vl-modulelist-weirdint-elim-aux x)))
Theorem:
(defthm vl-modulelist-weirdint-elim-aux-vl-modulelist-equiv-congruence-on-x (implies (vl-modulelist-equiv x x-equiv) (equal (vl-modulelist-weirdint-elim-aux x) (vl-modulelist-weirdint-elim-aux x-equiv))) :rule-classes :congruence)