		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svarlist-boundedp-badguy

Signature
(svarlist-boundedp-badguy x bound) → badguy
Arguments: x — Guard (svarlist-p x).; bound — Guard (natp bound).
Returns: badguy — Type (iff (svar-p badguy) badguy).

Definitions and Theorems

Function: svarlist-boundedp-badguy

(defun svarlist-boundedp-badguy (x bound)
  (declare (xargs :guard (and (svarlist-p x) (natp bound))))
  (let ((__function__ 'svarlist-boundedp-badguy))
    (declare (ignorable __function__))
    (if (atom x)
        (svar-set-index (address->svar (make-address :path ""))
                        bound)
      (if (svar-boundedp (car x) bound)
          (svarlist-boundedp-badguy (cdr x) bound)
        (svar-fix (car x))))))

Theorem: return-type-of-svarlist-boundedp-badguy

(defthm return-type-of-svarlist-boundedp-badguy
  (b* ((badguy (svarlist-boundedp-badguy x bound)))
    (iff (svar-p badguy) badguy))
  :rule-classes :rewrite)

Theorem: svarlist-boundedp-badguy-not-bounded

(defthm svarlist-boundedp-badguy-not-bounded
  (not (svar-boundedp (svarlist-boundedp-badguy x bound)
                      bound)))

Theorem: svarlist-boundedp-badguy-rw

(defthm svarlist-boundedp-badguy-rw
  (implies (acl2::rewriting-positive-literal
                (cons 'svarlist-boundedp
                      (cons x (cons bound 'nil))))
           (equal (svarlist-boundedp x bound)
                  (let ((badguy (svarlist-boundedp-badguy x bound)))
                    (not (member badguy (svarlist-fix x)))))))

Theorem: svarlist-boundedp-badguy-1

(defthm svarlist-boundedp-badguy-1
  (implies (not (member (svarlist-boundedp-badguy x bound)
                        (svarlist-fix x)))
           (svarlist-boundedp x bound)))

Theorem: svarlist-boundedp-badguy-not-member-when-bounded

(defthm svarlist-boundedp-badguy-not-member-when-bounded
  (implies (and (svarlist-boundedp x bound)
                (svarlist-p x))
           (not (member (svarlist-boundedp-badguy y bound)
                        x))))

Theorem: svarlist-boundedp-badguy-not-equal-svar-addr

(defthm svarlist-boundedp-badguy-not-equal-svar-addr
  (implies (svar-boundedp y bound)
           (not (equal (svarlist-boundedp-badguy x bound)
                       y))))

Theorem: svarlist-boundedp-badguy-of-svarlist-fix-x

(defthm svarlist-boundedp-badguy-of-svarlist-fix-x
  (equal (svarlist-boundedp-badguy (svarlist-fix x)
                                   bound)
         (svarlist-boundedp-badguy x bound)))

Theorem: svarlist-boundedp-badguy-svarlist-equiv-congruence-on-x

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

Theorem: svarlist-boundedp-badguy-of-nfix-bound

(defthm svarlist-boundedp-badguy-of-nfix-bound
  (equal (svarlist-boundedp-badguy x (nfix bound))
         (svarlist-boundedp-badguy x bound)))

Theorem: svarlist-boundedp-badguy-nat-equiv-congruence-on-bound

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