(svarlist-addr-p-badguy x) → badguy
Function:
(defun svarlist-addr-p-badguy (x) (declare (xargs :guard (svarlist-p x))) (let ((__function__ 'svarlist-addr-p-badguy)) (declare (ignorable __function__)) (if (atom x) (make-svar :name :not-an-address) (if (svar-addr-p (car x)) (svarlist-addr-p-badguy (cdr x)) (svar-fix (car x))))))
Theorem:
(defthm return-type-of-svarlist-addr-p-badguy (b* ((badguy (svarlist-addr-p-badguy x))) (iff (svar-p badguy) badguy)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-badguy-not-addr-p (not (svar-addr-p (svarlist-addr-p-badguy x))))
Theorem:
(defthm svarlist-addr-p-by-badguy (implies (not (member (svarlist-addr-p-badguy x) (svarlist-fix x))) (svarlist-addr-p x)))
Theorem:
(defthm svarlist-addr-p-badguy-not-member-when-addr-p (implies (and (svarlist-addr-p x) (svarlist-p x)) (not (member (svarlist-addr-p-badguy y) x))))
Theorem:
(defthm svarlist-addr-p-badguy-not-equal-svar-addr (implies (svar-addr-p y) (not (equal (svarlist-addr-p-badguy x) y))))
Theorem:
(defthm svarlist-addr-p-badguy-of-svarlist-fix-x (equal (svarlist-addr-p-badguy (svarlist-fix x)) (svarlist-addr-p-badguy x)))
Theorem:
(defthm svarlist-addr-p-badguy-svarlist-equiv-congruence-on-x (implies (svarlist-equiv x x-equiv) (equal (svarlist-addr-p-badguy x) (svarlist-addr-p-badguy x-equiv))) :rule-classes :congruence)