(sv::svarlist-remove-delays acl2::x) → sv::new-x
Function:
(defun sv::svarlist-remove-delays (acl2::x) (declare (xargs :guard (sv::svarlist-p acl2::x))) (let ((__function__ 'sv::svarlist-remove-delays)) (declare (ignorable __function__)) (if (atom acl2::x) nil (cons (b* (((sv::svar sv::x1) (car acl2::x))) (sv::make-svar :name sv::x1.name)) (sv::svarlist-remove-delays (cdr acl2::x))))))
Theorem:
(defthm sv::svarlist-p-of-svarlist-remove-delays (b* ((sv::new-x (sv::svarlist-remove-delays acl2::x))) (sv::svarlist-p sv::new-x)) :rule-classes :rewrite)
Theorem:
(defthm sv::svarlist-remove-delays-of-svarlist-fix-x (equal (sv::svarlist-remove-delays (sv::svarlist-fix acl2::x)) (sv::svarlist-remove-delays acl2::x)))
Theorem:
(defthm sv::svarlist-remove-delays-svarlist-equiv-congruence-on-x (implies (sv::svarlist-equiv acl2::x sv::x-equiv) (equal (sv::svarlist-remove-delays acl2::x) (sv::svarlist-remove-delays sv::x-equiv))) :rule-classes :congruence)