		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svar-subtract-delay

Signature
(svar-subtract-delay x delay) → xx
Arguments: x — Guard (svar-p x).; delay — Guard (natp delay).
Returns: xx — Type (svar-p xx).

Definitions and Theorems

Function: svar-subtract-delay

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

Theorem: svar-p-of-svar-subtract-delay

(defthm svar-p-of-svar-subtract-delay
  (b* ((xx (svar-subtract-delay x delay)))
    (svar-p xx))
  :rule-classes :rewrite)

Theorem: svar-addr-p-of-svar-subtract-delay

(defthm svar-addr-p-of-svar-subtract-delay
  (b* ((?xx (svar-subtract-delay x delay)))
    (iff (svar-addr-p xx) (svar-addr-p x))))

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

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

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

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

Theorem: svar-subtract-delay-of-nfix-delay

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

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

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