		Search-engine friendly clone of the ACL2 documentation.

Address

Svar-add-delay

Signature
(svar-add-delay x delay) → xx
Arguments: x — Guard (svar-p x).; delay — Guard (natp delay).
Returns: xx — Type (and (svar-p xx) (implies (svar-addr-p x) (svar-addr-p xx))).

Definitions and Theorems

Function: svar-add-delay

(defun svar-add-delay (x delay)
  (declare (xargs :guard (and (svar-p x) (natp delay))))
  (let ((__function__ 'svar-add-delay))
    (declare (ignorable __function__))
    (change-svar x
                 :delay (+ (lnfix delay) (svar->delay x)))))

Theorem: return-type-of-svar-add-delay

(defthm return-type-of-svar-add-delay
  (b* ((xx (svar-add-delay x delay)))
    (and (svar-p xx)
         (implies (svar-addr-p x)
                  (svar-addr-p xx))))
  :rule-classes :rewrite)

Theorem: svar-add-delay-when-zero

(defthm svar-add-delay-when-zero
  (equal (svar-add-delay x 0)
         (svar-fix x)))

Theorem: svar-add-delay-of-svar-fix-x

(defthm svar-add-delay-of-svar-fix-x
  (equal (svar-add-delay (svar-fix x) delay)
         (svar-add-delay x delay)))

Theorem: svar-add-delay-svar-equiv-congruence-on-x

(defthm svar-add-delay-svar-equiv-congruence-on-x
  (implies (svar-equiv x x-equiv)
           (equal (svar-add-delay x delay)
                  (svar-add-delay x-equiv delay)))
  :rule-classes :congruence)

Theorem: svar-add-delay-of-nfix-delay

(defthm svar-add-delay-of-nfix-delay
  (equal (svar-add-delay x (nfix delay))
         (svar-add-delay x delay)))

Theorem: svar-add-delay-nat-equiv-congruence-on-delay

(defthm svar-add-delay-nat-equiv-congruence-on-delay
  (implies (nat-equiv delay delay-equiv)
           (equal (svar-add-delay x delay)
                  (svar-add-delay x delay-equiv)))
  :rule-classes :congruence)