		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svar-idxaddr-okp

Signature
(svar-idxaddr-okp x bound) → *
Arguments: x — Guard (svar-p x).; bound — Guard (natp bound).

Definitions and Theorems

Function: svar-idxaddr-okp

(defun svar-idxaddr-okp (x bound)
  (declare (xargs :guard (and (svar-p x) (natp bound))))
  (let ((__function__ 'svar-idxaddr-okp))
    (declare (ignorable __function__))
    (and (svar-addr-p x)
         (b* ((addr (svar->address x))
              ((address addr)))
           (or (not addr.index)
               (< addr.index (lnfix bound)))))))

Theorem: svar-idxaddr-okp-of-svar-fix-x

(defthm svar-idxaddr-okp-of-svar-fix-x
  (equal (svar-idxaddr-okp (svar-fix x) bound)
         (svar-idxaddr-okp x bound)))

Theorem: svar-idxaddr-okp-svar-equiv-congruence-on-x

(defthm svar-idxaddr-okp-svar-equiv-congruence-on-x
  (implies (svar-equiv x x-equiv)
           (equal (svar-idxaddr-okp x bound)
                  (svar-idxaddr-okp x-equiv bound)))
  :rule-classes :congruence)

Theorem: svar-idxaddr-okp-of-nfix-bound

(defthm svar-idxaddr-okp-of-nfix-bound
  (equal (svar-idxaddr-okp x (nfix bound))
         (svar-idxaddr-okp x bound)))

Theorem: svar-idxaddr-okp-nat-equiv-congruence-on-bound

(defthm svar-idxaddr-okp-nat-equiv-congruence-on-bound
  (implies (nat-equiv bound bound-equiv)
           (equal (svar-idxaddr-okp x bound)
                  (svar-idxaddr-okp x bound-equiv)))
  :rule-classes :congruence)

Theorem: svar-idxaddr-okp-of-greater

(defthm svar-idxaddr-okp-of-greater
  (implies (and (svar-idxaddr-okp x bound1)
                (<= (nfix bound1) (nfix bound2)))
           (svar-idxaddr-okp x bound2)))

Theorem: svar-addr-p-when-svar-idxadrr-okp

(defthm svar-addr-p-when-svar-idxadrr-okp
  (implies (svar-idxaddr-okp x bound)
           (svar-addr-p x))
  :rule-classes (:rewrite :forward-chaining))