		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Delay-svar->delays

Signature
(delay-svar->delays x) → delays
Arguments: x — Guard (svar-p x).
Returns: delays — Type (svar-map-p delays).

Definitions and Theorems

Function: delay-svar->delays

(defun delay-svar->delays (x)
  (declare (xargs :guard (svar-p x)))
  (let ((__function__ 'delay-svar->delays))
    (declare (ignorable __function__))
    (b* (((svar x) (svar-fix x))
         ((when (eql 0 x.delay)) nil)
         (next-x (change-svar x :delay (1- x.delay)))
         (pair (cons x next-x)))
      (cons pair (delay-svar->delays next-x)))))

Theorem: svar-map-p-of-delay-svar->delays

(defthm svar-map-p-of-delay-svar->delays
  (b* ((delays (delay-svar->delays x)))
    (svar-map-p delays))
  :rule-classes :rewrite)

Theorem: vars-of-delay-svar->delays

(defthm vars-of-delay-svar->delays
  (b* ((?delays (delay-svar->delays x)))
    (implies (svar-addr-p x)
             (svarlist-addr-p (svar-map-vars delays)))))

Theorem: vars-of-delay-svar->delays-keys

(defthm vars-of-delay-svar->delays-keys
  (b* ((?delays (delay-svar->delays x)))
    (implies (svar-addr-p x)
             (svarlist-addr-p (alist-keys delays)))))

Theorem: vars-of-delay-svar->delays-vals

(defthm vars-of-delay-svar->delays-vals
  (b* ((?delays (delay-svar->delays x)))
    (implies (svar-addr-p x)
             (svarlist-addr-p (alist-vals delays)))))

Theorem: delay-svar->delays-of-svar-fix-x

(defthm delay-svar->delays-of-svar-fix-x
  (equal (delay-svar->delays (svar-fix x))
         (delay-svar->delays x)))

Theorem: delay-svar->delays-svar-equiv-congruence-on-x

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