		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svar-boundedp

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

Definitions and Theorems

Function: svar-boundedp

(defun svar-boundedp (x bound)
  (declare (xargs :guard (and (svar-p x) (natp bound))))
  (let ((__function__ 'svar-boundedp))
    (declare (ignorable __function__))
    (and (svar-indexedp x)
         (b* ((i (svar-index x)))
           (< i (lnfix bound))))))

Theorem: svar-boundedp-of-svar-fix-x

(defthm svar-boundedp-of-svar-fix-x
  (equal (svar-boundedp (svar-fix x) bound)
         (svar-boundedp x bound)))

Theorem: svar-boundedp-svar-equiv-congruence-on-x

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

Theorem: svar-boundedp-of-nfix-bound

(defthm svar-boundedp-of-nfix-bound
  (equal (svar-boundedp x (nfix bound))
         (svar-boundedp x bound)))

Theorem: svar-boundedp-nat-equiv-congruence-on-bound

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

Theorem: svar-boundedp-of-greater

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

Theorem: svar-boundedp-implies-svar-indexedp

(defthm svar-boundedp-implies-svar-indexedp
  (implies (svar-boundedp x bound)
           (and (svar-indexedp x)
                (< (svar-index x) (nfix bound))
                (implies (natp bound)
                         (< (svar-index x) (nfix bound)))))
  :rule-classes :forward-chaining)

Theorem: svar-boundedp-of-svar-set-index

(defthm svar-boundedp-of-svar-set-index
  (iff (svar-boundedp (svar-set-index x idx)
                      bound)
       (< (nfix idx) (nfix bound))))