(svar-delayed-member v x) → *
Function:
(defun svar-delayed-member (v x) (declare (xargs :guard (and (svar-p v) (svarlist-p x)))) (let ((__function__ 'svar-delayed-member)) (declare (ignorable __function__)) (if (atom x) nil (if (equal (svar->name v) (svar->name (car x))) (svarlist-fix x) (svar-delayed-member v (cdr x))))))
Theorem:
(defthm svar-delayed-member-of-svar-fix-v (equal (svar-delayed-member (svar-fix v) x) (svar-delayed-member v x)))
Theorem:
(defthm svar-delayed-member-svar-equiv-congruence-on-v (implies (svar-equiv v v-equiv) (equal (svar-delayed-member v x) (svar-delayed-member v-equiv x))) :rule-classes :congruence)
Theorem:
(defthm svar-delayed-member-of-svarlist-fix-x (equal (svar-delayed-member v (svarlist-fix x)) (svar-delayed-member v x)))
Theorem:
(defthm svar-delayed-member-svarlist-equiv-congruence-on-x (implies (svarlist-equiv x x-equiv) (equal (svar-delayed-member v x) (svar-delayed-member v x-equiv))) :rule-classes :congruence)