		Search-engine friendly clone of the ACL2 documentation.

Svarlist-idxaddr-okp

Svarlist-idxaddr-okp-basics

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

Definitions and Theorems

Theorem: svarlist-idxaddr-okp-of-cons

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

Theorem: svarlist-idxaddr-okp-of-cdr-when-svarlist-idxaddr-okp

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

Theorem: svarlist-idxaddr-okp-when-not-consp

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

Theorem: svar-idxaddr-okp-of-car-when-svarlist-idxaddr-okp

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

Theorem: svarlist-idxaddr-okp-of-append

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

Theorem: svarlist-idxaddr-okp-of-list-fix

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

Theorem: svarlist-idxaddr-okp-of-rev

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

Theorem: svarlist-idxaddr-okp-of-repeat

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

Theorem: svarlist-idxaddr-okp-of-update-nth

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

Theorem: svar-idxaddr-okp-of-nth-when-svarlist-idxaddr-okp

(defthm svar-idxaddr-okp-of-nth-when-svarlist-idxaddr-okp
  (implies (and (svarlist-idxaddr-okp x bound)
                (< (nfix acl2::n) (len x)))
           (svar-idxaddr-okp (nth acl2::n x)
                             bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-take

(defthm svarlist-idxaddr-okp-of-take
  (implies (svarlist-idxaddr-okp (double-rewrite x)
                                 bound)
           (iff (svarlist-idxaddr-okp (take acl2::n x)
                                      bound)
                (or (svar-idxaddr-okp nil bound)
                    (<= (nfix acl2::n) (len x)))))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-rcons

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

Theorem: svar-idxaddr-okp-when-member-equal-of-svarlist-idxaddr-okp

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

Theorem: svarlist-idxaddr-okp-when-subsetp-equal

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

Theorem: svarlist-idxaddr-okp-set-equiv-congruence

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

Theorem: svarlist-idxaddr-okp-of-set-difference-equal

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

Theorem: svarlist-idxaddr-okp-of-intersection-equal-1

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

Theorem: svarlist-idxaddr-okp-of-intersection-equal-2

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

Theorem: svarlist-idxaddr-okp-of-union-equal

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

Theorem: svarlist-idxaddr-okp-of-sfix

(defthm svarlist-idxaddr-okp-of-sfix
  (iff (svarlist-idxaddr-okp (sfix x) bound)
       (or (svarlist-idxaddr-okp x bound)
           (not (setp x))))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-insert

(defthm svarlist-idxaddr-okp-of-insert
  (iff (svarlist-idxaddr-okp (insert acl2::a x)
                             bound)
       (and (svarlist-idxaddr-okp (sfix x) bound)
            (svar-idxaddr-okp acl2::a bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-delete

(defthm svarlist-idxaddr-okp-of-delete
  (implies (svarlist-idxaddr-okp x bound)
           (svarlist-idxaddr-okp (delete acl2::k x)
                                 bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-mergesort

(defthm svarlist-idxaddr-okp-of-mergesort
  (iff (svarlist-idxaddr-okp (mergesort x)
                             bound)
       (svarlist-idxaddr-okp (list-fix x)
                             bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-union

(defthm svarlist-idxaddr-okp-of-union
  (iff (svarlist-idxaddr-okp (union x y) bound)
       (and (svarlist-idxaddr-okp (sfix x) bound)
            (svarlist-idxaddr-okp (sfix y) bound)))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-intersect-1

(defthm svarlist-idxaddr-okp-of-intersect-1
  (implies (svarlist-idxaddr-okp x bound)
           (svarlist-idxaddr-okp (intersect x y)
                                 bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-intersect-2

(defthm svarlist-idxaddr-okp-of-intersect-2
  (implies (svarlist-idxaddr-okp y bound)
           (svarlist-idxaddr-okp (intersect x y)
                                 bound))
  :rule-classes ((:rewrite)))

Theorem: svarlist-idxaddr-okp-of-difference

(defthm svarlist-idxaddr-okp-of-difference
  (implies (svarlist-idxaddr-okp x bound)
           (svarlist-idxaddr-okp (difference x y)
                                 bound))
  :rule-classes ((:rewrite)))