For error reporting, find an arg that has a problem.
(vl-first-bad-gatearg-for-delayredux x) → *
Function:
(defun vl-first-bad-gatearg-for-delayredux (x) (declare (xargs :guard (vl-plainarglist-p x))) (let ((__function__ 'vl-first-bad-gatearg-for-delayredux)) (declare (ignorable __function__)) (cond ((atom x) nil) ((vl-gatearg-ok-for-delayredux-p (car x)) (vl-first-bad-gatearg-for-delayredux (cdr x))) (t (car x)))))
Theorem:
(defthm vl-first-bad-gatearg-for-delayredux-under-iff (implies (force (vl-plainarglist-p x)) (iff (vl-first-bad-gatearg-for-delayredux x) (not (vl-gateargs-ok-for-delayredux-p x)))))
Theorem:
(defthm vl-plainarg-p-of-vl-first-bad-gatearg-for-delayredux (implies (force (vl-plainarglist-p x)) (equal (vl-plainarg-p (vl-first-bad-gatearg-for-delayredux x)) (not (vl-gateargs-ok-for-delayredux-p x)))))