(svarlist-add-delay x delay) maps svar-add-delay across a list.
(svarlist-add-delay x delay) → xx
This is an ordinary defprojection.
Function:
(defun svarlist-add-delay-exec (x delay acc) (declare (xargs :guard (and (svarlist-p x) (natp delay)))) (declare (xargs :guard t)) (let ((__function__ 'svarlist-add-delay-exec)) (declare (ignorable __function__)) (if (consp x) (svarlist-add-delay-exec (cdr x) delay (cons (svar-add-delay (car x) delay) acc)) acc)))
Function:
(defun svarlist-add-delay-nrev (x delay acl2::nrev) (declare (xargs :stobjs (acl2::nrev))) (declare (xargs :guard (and (svarlist-p x) (natp delay)))) (declare (xargs :guard t)) (let ((__function__ 'svarlist-add-delay-nrev)) (declare (ignorable __function__)) (if (atom x) (acl2::nrev-fix acl2::nrev) (let ((acl2::nrev (acl2::nrev-push (svar-add-delay (car x) delay) acl2::nrev))) (svarlist-add-delay-nrev (cdr x) delay acl2::nrev)))))
Function:
(defun svarlist-add-delay (x delay) (declare (xargs :guard (and (svarlist-p x) (natp delay)))) (declare (xargs :guard t)) (let ((__function__ 'svarlist-add-delay)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (cons (svar-add-delay (car x) delay) (svarlist-add-delay (cdr x) delay)) nil) :exec (if (atom x) nil (acl2::with-local-nrev (svarlist-add-delay-nrev x delay acl2::nrev))))))
Theorem:
(defthm return-type-of-svarlist-add-delay (b* ((xx (svarlist-add-delay x delay))) (and (svarlist-p xx) (implies (svarlist-addr-p x) (svarlist-addr-p xx)))) :rule-classes :rewrite)
Theorem:
(defthm svarlist-add-delay-of-svarlist-fix-x (equal (svarlist-add-delay (svarlist-fix x) delay) (svarlist-add-delay x delay)))
Theorem:
(defthm svarlist-add-delay-svarlist-equiv-congruence-on-x (implies (svarlist-equiv x x-equiv) (equal (svarlist-add-delay x delay) (svarlist-add-delay x-equiv delay))) :rule-classes :congruence)
Theorem:
(defthm svarlist-add-delay-of-nfix-delay (equal (svarlist-add-delay x (nfix delay)) (svarlist-add-delay x delay)))
Theorem:
(defthm svarlist-add-delay-nat-equiv-congruence-on-delay (implies (nat-equiv delay delay-equiv) (equal (svarlist-add-delay x delay) (svarlist-add-delay x delay-equiv))) :rule-classes :congruence)
Theorem:
(defthm set-equiv-congruence-over-svarlist-add-delay (implies (set-equiv x y) (set-equiv (svarlist-add-delay x delay) (svarlist-add-delay y delay))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-svarlist-add-delay-when-subsetp (implies (subsetp x y) (subsetp (svarlist-add-delay x delay) (svarlist-add-delay y delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-of-svar-add-delay-in-svarlist-add-delay (implies (member acl2::k x) (member (svar-add-delay acl2::k delay) (svarlist-add-delay x delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-nrev-removal (equal (svarlist-add-delay-nrev x delay acl2::nrev) (append acl2::nrev (svarlist-add-delay x delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-exec-removal (equal (svarlist-add-delay-exec x delay acl2::acc) (revappend (svarlist-add-delay x delay) acl2::acc)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-of-rev (equal (svarlist-add-delay (rev x) delay) (rev (svarlist-add-delay x delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-of-list-fix (equal (svarlist-add-delay (list-fix x) delay) (svarlist-add-delay x delay)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-of-append (equal (svarlist-add-delay (append acl2::a acl2::b) delay) (append (svarlist-add-delay acl2::a delay) (svarlist-add-delay acl2::b delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm cdr-of-svarlist-add-delay (equal (cdr (svarlist-add-delay x delay)) (svarlist-add-delay (cdr x) delay)) :rule-classes ((:rewrite)))
Theorem:
(defthm car-of-svarlist-add-delay (equal (car (svarlist-add-delay x delay)) (and (consp x) (svar-add-delay (car x) delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-under-iff (iff (svarlist-add-delay x delay) (consp x)) :rule-classes ((:rewrite)))
Theorem:
(defthm consp-of-svarlist-add-delay (equal (consp (svarlist-add-delay x delay)) (consp x)) :rule-classes ((:rewrite)))
Theorem:
(defthm len-of-svarlist-add-delay (equal (len (svarlist-add-delay x delay)) (len x)) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-of-svarlist-add-delay (true-listp (svarlist-add-delay x delay)) :rule-classes :type-prescription)
Theorem:
(defthm svarlist-add-delay-when-not-consp (implies (not (consp x)) (equal (svarlist-add-delay x delay) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-of-cons (equal (svarlist-add-delay (cons acl2::a acl2::b) delay) (cons (svar-add-delay acl2::a delay) (svarlist-add-delay acl2::b delay))) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-add-delay-when-0 (equal (svarlist-add-delay x 0) (svarlist-fix x)))