		Search-engine friendly clone of the ACL2 documentation.

Svarlist-boundedp

Svarlist-boundedp-basics

Basic theorems about svarlist-boundedp, generated by std::deflist.

Definitions and Theorems

Theorem: svarlist-boundedp-of-cons

(defthm svarlist-boundedp-of-cons
  (equal (svarlist-boundedp (cons acl2::a x)
                            bound)
         (and (svar-boundedp acl2::a bound)
              (svarlist-boundedp x bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-cdr-when-svarlist-boundedp

(defthm svarlist-boundedp-of-cdr-when-svarlist-boundedp
  (implies (svarlist-boundedp (double-rewrite x)
                              bound)
           (svarlist-boundedp (cdr x) bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-when-not-consp

(defthm svarlist-boundedp-when-not-consp
  (implies (not (consp x))
           (svarlist-boundedp x bound))
  :rule-classes ((:rewrite)))

Theorem: svar-boundedp-of-car-when-svarlist-boundedp

(defthm svar-boundedp-of-car-when-svarlist-boundedp
  (implies (svarlist-boundedp x bound)
           (iff (svar-boundedp (car x) bound)
                (or (consp x)
                    (svar-boundedp nil bound))))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-append

(defthm svarlist-boundedp-of-append
  (equal (svarlist-boundedp (append acl2::a acl2::b)
                            bound)
         (and (svarlist-boundedp acl2::a bound)
              (svarlist-boundedp acl2::b bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-list-fix

(defthm svarlist-boundedp-of-list-fix
  (equal (svarlist-boundedp (list-fix x) bound)
         (svarlist-boundedp x bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-rev

(defthm svarlist-boundedp-of-rev
  (equal (svarlist-boundedp (rev x) bound)
         (svarlist-boundedp (list-fix x) bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-repeat

(defthm svarlist-boundedp-of-repeat
  (iff (svarlist-boundedp (repeat acl2::n x)
                          bound)
       (or (svar-boundedp x bound)
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-rcons

(defthm svarlist-boundedp-of-rcons
  (iff (svarlist-boundedp (acl2::rcons acl2::a x)
                          bound)
       (and (svar-boundedp acl2::a bound)
            (svarlist-boundedp (list-fix x) bound)))
  :rule-classes ((:rewrite)))

Theorem: svar-boundedp-when-member-equal-of-svarlist-boundedp

(defthm svar-boundedp-when-member-equal-of-svarlist-boundedp
  (and (implies (and (member-equal acl2::a x)
                     (svarlist-boundedp x bound))
                (svar-boundedp acl2::a bound))
       (implies (and (svarlist-boundedp x bound)
                     (member-equal acl2::a x))
                (svar-boundedp acl2::a bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-when-subsetp-equal

(defthm svarlist-boundedp-when-subsetp-equal
  (and (implies (and (subsetp-equal x y)
                     (svarlist-boundedp y bound))
                (svarlist-boundedp x bound))
       (implies (and (svarlist-boundedp y bound)
                     (subsetp-equal x y))
                (svarlist-boundedp x bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-set-equiv-congruence

(defthm svarlist-boundedp-set-equiv-congruence
  (implies (set-equiv x y)
           (equal (svarlist-boundedp x bound)
                  (svarlist-boundedp y bound)))
  :rule-classes :congruence)

Theorem: svarlist-boundedp-of-set-difference-equal

(defthm svarlist-boundedp-of-set-difference-equal
  (implies (svarlist-boundedp x bound)
           (svarlist-boundedp (set-difference-equal x y)
                              bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-intersection-equal-1

(defthm svarlist-boundedp-of-intersection-equal-1
  (implies (svarlist-boundedp (double-rewrite x)
                              bound)
           (svarlist-boundedp (intersection-equal x y)
                              bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-intersection-equal-2

(defthm svarlist-boundedp-of-intersection-equal-2
  (implies (svarlist-boundedp (double-rewrite y)
                              bound)
           (svarlist-boundedp (intersection-equal x y)
                              bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-union-equal

(defthm svarlist-boundedp-of-union-equal
  (equal (svarlist-boundedp (union-equal x y)
                            bound)
         (and (svarlist-boundedp (list-fix x) bound)
              (svarlist-boundedp (double-rewrite y)
                                 bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-update-nth

(defthm svarlist-boundedp-of-update-nth
  (implies (svarlist-boundedp (double-rewrite x)
                              bound)
           (iff (svarlist-boundedp (update-nth acl2::n y x)
                                   bound)
                (and (svar-boundedp y bound)
                     (or (<= (nfix acl2::n) (len x))
                         (svar-boundedp nil bound)))))
  :rule-classes ((:rewrite)))

Theorem: svarlist-boundedp-of-butlast

(defthm svarlist-boundedp-of-butlast
  (implies (svarlist-boundedp (double-rewrite x)
                              bound)
           (svarlist-boundedp (butlast x acl2::n)
                              bound))
  :rule-classes ((:rewrite)))