(svtv-non-override-test-input-vars x map) → new-x
Function:
(defun svtv-non-override-test-input-vars (x map) (declare (xargs :guard (and (svarlist-p x) (svtv-inputmap-p map)))) (let ((__function__ 'svtv-non-override-test-input-vars)) (declare (ignorable __function__)) (if (atom x) nil (if (eq (cdr (hons-get (svar-fix (car x)) (svtv-inputmap-fix map))) :override-test) (svtv-non-override-test-input-vars (cdr x) map) (cons (svar-fix (car x)) (svtv-non-override-test-input-vars (cdr x) map))))))
Theorem:
(defthm svarlist-p-of-svtv-non-override-test-input-vars (b* ((new-x (svtv-non-override-test-input-vars x map))) (svarlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm svtv-non-override-test-input-vars-of-svarlist-fix-x (equal (svtv-non-override-test-input-vars (svarlist-fix x) map) (svtv-non-override-test-input-vars x map)))
Theorem:
(defthm svtv-non-override-test-input-vars-svarlist-equiv-congruence-on-x (implies (svarlist-equiv x x-equiv) (equal (svtv-non-override-test-input-vars x map) (svtv-non-override-test-input-vars x-equiv map))) :rule-classes :congruence)
Theorem:
(defthm svtv-non-override-test-input-vars-of-svtv-inputmap-fix-map (equal (svtv-non-override-test-input-vars x (svtv-inputmap-fix map)) (svtv-non-override-test-input-vars x map)))
Theorem:
(defthm svtv-non-override-test-input-vars-svtv-inputmap-equiv-congruence-on-map (implies (svtv-inputmap-equiv map map-equiv) (equal (svtv-non-override-test-input-vars x map) (svtv-non-override-test-input-vars x map-equiv))) :rule-classes :congruence)