(vl-modulelist-weirdint-elim x) → new-x
Function:
(defun vl-modulelist-weirdint-elim (x) (declare (xargs :guard (vl-modulelist-p x))) (let ((__function__ 'vl-modulelist-weirdint-elim)) (declare (ignorable __function__)) (b* (((mv x-prime new-mods) (vl-modulelist-weirdint-elim-aux x)) (new-mods (mergesort new-mods)) (full-mods (mergesort (append new-mods x-prime))) ((unless (uniquep (vl-modulelist->names full-mods))) (raise "Name collision!"))) full-mods)))
Theorem:
(defthm vl-modulelist-p-of-vl-modulelist-weirdint-elim (b* ((new-x (vl-modulelist-weirdint-elim x))) (vl-modulelist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-modulelist-weirdint-elim-of-vl-modulelist-fix-x (equal (vl-modulelist-weirdint-elim (vl-modulelist-fix x)) (vl-modulelist-weirdint-elim x)))
Theorem:
(defthm vl-modulelist-weirdint-elim-vl-modulelist-equiv-congruence-on-x (implies (vl-modulelist-equiv x x-equiv) (equal (vl-modulelist-weirdint-elim x) (vl-modulelist-weirdint-elim x-equiv))) :rule-classes :congruence)