Creates a substitution alist that maps the given variables to their 1-tick delayed versions. Warns if the variables aren't of the expected form.
(sv::svarlist-delay-subst acl2::x) → subst
Function:
(defun sv::svarlist-delay-subst (acl2::x) (declare (xargs :guard (sv::svarlist-p acl2::x))) (let ((__function__ 'sv::svarlist-delay-subst)) (declare (ignorable __function__)) (if (atom acl2::x) nil (cons (cons (sv::svar-fix (car acl2::x)) (sv::make-svex-var :name (sv::svar-add-delay (car acl2::x) 1))) (sv::svarlist-delay-subst (cdr acl2::x))))))
Theorem:
(defthm sv::svex-alist-p-of-svarlist-delay-subst (b* ((subst (sv::svarlist-delay-subst acl2::x))) (sv::svex-alist-p subst)) :rule-classes :rewrite)
Theorem:
(defthm sv::vars-of-svarlist-delay-subst (implies (sv::svarlist-addr-p acl2::x) (sv::svarlist-addr-p (sv::svex-alist-vars (sv::svarlist-delay-subst acl2::x)))))
Theorem:
(defthm sv::keys-of-svarlist-delay-subst (implies (and (not (member sv::v (sv::svarlist-fix acl2::x))) (sv::svar-p sv::v)) (not (sv::svex-lookup sv::v (sv::svarlist-delay-subst acl2::x)))))
Theorem:
(defthm sv::svarlist-delay-subst-of-svarlist-fix-x (equal (sv::svarlist-delay-subst (sv::svarlist-fix acl2::x)) (sv::svarlist-delay-subst acl2::x)))
Theorem:
(defthm sv::svarlist-delay-subst-svarlist-equiv-congruence-on-x (implies (sv::svarlist-equiv acl2::x sv::x-equiv) (equal (sv::svarlist-delay-subst acl2::x) (sv::svarlist-delay-subst sv::x-equiv))) :rule-classes :congruence)