(svex-alist-add-delay x delay) → new-x
Function:
(defun svex-alist-add-delay (x delay) (declare (xargs :guard (and (svex-alist-p x) (natp delay)))) (let ((__function__ 'svex-alist-add-delay)) (declare (ignorable __function__)) (b* ((ans (pairlis$ (svex-alist-keys x) (svexlist-add-delay (svex-alist-vals x) delay)))) (clear-memoize-table 'svex-add-delay) ans)))
Theorem:
(defthm svex-alist-p-of-svex-alist-add-delay (b* ((new-x (svex-alist-add-delay x delay))) (svex-alist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm keys-of-svex-alist-add-delay (b* ((new-x (svex-alist-add-delay x delay))) (iff (svex-lookup v new-x) (svex-lookup v x))) :rule-classes :rewrite)
Theorem:
(defthm vars-of-svex-alist-add-delay (b* ((new-x (svex-alist-add-delay x delay))) (implies (svarlist-addr-p (svex-alist-vars x)) (svarlist-addr-p (svex-alist-vars new-x)))) :rule-classes :rewrite)
Theorem:
(defthm svex-alist-add-delay-of-svex-alist-fix-x (equal (svex-alist-add-delay (svex-alist-fix x) delay) (svex-alist-add-delay x delay)))
Theorem:
(defthm svex-alist-add-delay-svex-alist-equiv-congruence-on-x (implies (svex-alist-equiv x x-equiv) (equal (svex-alist-add-delay x delay) (svex-alist-add-delay x-equiv delay))) :rule-classes :congruence)
Theorem:
(defthm svex-alist-add-delay-of-nfix-delay (equal (svex-alist-add-delay x (nfix delay)) (svex-alist-add-delay x delay)))
Theorem:
(defthm svex-alist-add-delay-nat-equiv-congruence-on-delay (implies (nat-equiv delay delay-equiv) (equal (svex-alist-add-delay x delay) (svex-alist-add-delay x delay-equiv))) :rule-classes :congruence)