(vl-collect-toobig-constant-atoms width x) → toobig
Function:
(defun vl-collect-toobig-constant-atoms (width x) (declare (xargs :guard (and (natp width) (vl-exprlist-p x)))) (let ((__function__ 'vl-collect-toobig-constant-atoms)) (declare (ignorable __function__)) (cond ((atom x) nil) ((vl-toobig-constant-atom-p width (car x)) (cons (vl-expr-fix (car x)) (vl-collect-toobig-constant-atoms width (cdr x)))) (t (vl-collect-toobig-constant-atoms width (cdr x))))))
Theorem:
(defthm vl-exprlist-p-of-vl-collect-toobig-constant-atoms (b* ((toobig (vl-collect-toobig-constant-atoms width x))) (vl-exprlist-p toobig)) :rule-classes :rewrite)
Theorem:
(defthm vl-collect-toobig-constant-atoms-of-nfix-width (equal (vl-collect-toobig-constant-atoms (nfix width) x) (vl-collect-toobig-constant-atoms width x)))
Theorem:
(defthm vl-collect-toobig-constant-atoms-nat-equiv-congruence-on-width (implies (acl2::nat-equiv width width-equiv) (equal (vl-collect-toobig-constant-atoms width x) (vl-collect-toobig-constant-atoms width-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-collect-toobig-constant-atoms-of-vl-exprlist-fix-x (equal (vl-collect-toobig-constant-atoms width (vl-exprlist-fix x)) (vl-collect-toobig-constant-atoms width x)))
Theorem:
(defthm vl-collect-toobig-constant-atoms-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-collect-toobig-constant-atoms width x) (vl-collect-toobig-constant-atoms width x-equiv))) :rule-classes :congruence)