Basic theorems about svarlist-idxaddr-okp, generated by std::deflist.
Theorem:
(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:
(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:
(defthm svarlist-idxaddr-okp-when-not-consp (implies (not (consp x)) (svarlist-idxaddr-okp x bound)) :rule-classes ((:rewrite)))
Theorem:
(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:
(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:
(defthm svarlist-idxaddr-okp-of-list-fix (equal (svarlist-idxaddr-okp (list-fix x) bound) (svarlist-idxaddr-okp x bound)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-idxaddr-okp-of-rev (equal (svarlist-idxaddr-okp (rev x) bound) (svarlist-idxaddr-okp (list-fix x) bound)) :rule-classes ((:rewrite)))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm svarlist-idxaddr-okp-of-delete (implies (svarlist-idxaddr-okp x bound) (svarlist-idxaddr-okp (delete acl2::k x) bound)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-idxaddr-okp-of-mergesort (iff (svarlist-idxaddr-okp (mergesort x) bound) (svarlist-idxaddr-okp (list-fix x) bound)) :rule-classes ((:rewrite)))
Theorem:
(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:
(defthm svarlist-idxaddr-okp-of-intersect-1 (implies (svarlist-idxaddr-okp x bound) (svarlist-idxaddr-okp (intersect x y) bound)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-idxaddr-okp-of-intersect-2 (implies (svarlist-idxaddr-okp y bound) (svarlist-idxaddr-okp (intersect x y) bound)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-idxaddr-okp-of-difference (implies (svarlist-idxaddr-okp x bound) (svarlist-idxaddr-okp (difference x y) bound)) :rule-classes ((:rewrite)))