(vl-exprdistlist-strip x) → new-x
Function:
(defun vl-exprdistlist-strip (x) (declare (xargs :guard (vl-exprdistlist-p x))) (let ((__function__ 'vl-exprdistlist-strip)) (declare (ignorable __function__)) (b* (((when (atom x)) (b* nil x)) (car (vl-exprdist-strip (car x))) (cdr (vl-exprdistlist-strip (cdr x)))) (cons-with-hint car cdr x))))
Theorem:
(defthm vl-exprdistlist-p-of-vl-exprdistlist-strip (b* ((new-x (vl-exprdistlist-strip x))) (vl-exprdistlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprdistlist-strip-of-vl-exprdistlist-fix-x (equal (vl-exprdistlist-strip (vl-exprdistlist-fix x)) (vl-exprdistlist-strip x)))
Theorem:
(defthm vl-exprdistlist-strip-vl-exprdistlist-equiv-congruence-on-x (implies (vl-exprdistlist-equiv x x-equiv) (equal (vl-exprdistlist-strip x) (vl-exprdistlist-strip x-equiv))) :rule-classes :congruence)