Basic theorems about svarlist-boundedp, generated by std::deflist.
Theorem:
(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:
(defthm svarlist-boundedp-of-cdr-when-svarlist-boundedp (implies (svarlist-boundedp (double-rewrite x) bound) (svarlist-boundedp (cdr x) bound)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-boundedp-when-not-consp (implies (not (consp x)) (svarlist-boundedp x bound)) :rule-classes ((:rewrite)))
Theorem:
(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:
(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:
(defthm svarlist-boundedp-of-list-fix (equal (svarlist-boundedp (list-fix x) bound) (svarlist-boundedp x bound)) :rule-classes ((:rewrite)))
Theorem:
(defthm svarlist-boundedp-of-rev (equal (svarlist-boundedp (rev x) bound) (svarlist-boundedp (list-fix x) bound)) :rule-classes ((:rewrite)))
Theorem:
(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:
(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:
(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:
(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:
(defthm svarlist-boundedp-set-equiv-congruence (implies (set-equiv x y) (equal (svarlist-boundedp x bound) (svarlist-boundedp y bound))) :rule-classes :congruence)
Theorem:
(defthm svarlist-boundedp-of-set-difference-equal (implies (svarlist-boundedp x bound) (svarlist-boundedp (set-difference-equal x y) bound)) :rule-classes ((:rewrite)))
Theorem:
(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:
(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:
(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:
(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:
(defthm svarlist-boundedp-of-butlast (implies (svarlist-boundedp (double-rewrite x) bound) (svarlist-boundedp (butlast x acl2::n) bound)) :rule-classes ((:rewrite)))