Basic theorems about list-in, generated by std::deflist.
Theorem:
(defthm list-in-of-cons (equal (list-in (cons a x) set) (and (in a set) (list-in x set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-cdr-when-list-in (implies (list-in (double-rewrite x) set) (list-in (cdr x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-when-not-consp (implies (not (consp x)) (list-in x set)) :rule-classes ((:rewrite)))
Theorem:
(defthm in-of-car-when-list-in (implies (list-in x set) (iff (in (car x) set) (or (consp x) (in nil set)))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-append (equal (list-in (append a b) set) (and (list-in a set) (list-in b set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-list-fix (equal (list-in (acl2::list-fix x) set) (list-in x set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-sfix (iff (list-in (sfix x) set) (or (list-in x set) (not (setp x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-insert (iff (list-in (insert a x) set) (and (list-in (sfix x) set) (in a set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-delete (implies (list-in x set) (list-in (delete k x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-mergesort (iff (list-in (mergesort x) set) (list-in (acl2::list-fix x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-union (iff (list-in (union x y) set) (and (list-in (sfix x) set) (list-in (sfix y) set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-intersect-1 (implies (list-in x set) (list-in (intersect x y) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-intersect-2 (implies (list-in y set) (list-in (intersect x y) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-difference (implies (list-in x set) (list-in (difference x y) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-duplicated-members (implies (list-in x set) (list-in (acl2::duplicated-members x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-rev (equal (list-in (acl2::rev x) set) (list-in (acl2::list-fix x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-rcons (iff (list-in (acl2::rcons a x) set) (and (in a set) (list-in (acl2::list-fix x) set))) :rule-classes ((:rewrite)))
Theorem:
(defthm in-when-member-equal-of-list-in (and (implies (and (member-equal a x) (list-in x set)) (in a set)) (implies (and (list-in x set) (member-equal a x)) (in a set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-when-subsetp-equal (and (implies (and (subsetp-equal x y) (list-in y set)) (list-in x set)) (implies (and (list-in y set) (subsetp-equal x y)) (list-in x set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-set-equiv-congruence (implies (acl2::set-equiv x y) (equal (list-in x set) (list-in y set))) :rule-classes :congruence)
Theorem:
(defthm list-in-of-set-difference-equal (implies (list-in x set) (list-in (set-difference-equal x y) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-intersection-equal-1 (implies (list-in (double-rewrite x) set) (list-in (intersection-equal x y) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-intersection-equal-2 (implies (list-in (double-rewrite y) set) (list-in (intersection-equal x y) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-union-equal (equal (list-in (union-equal x y) set) (and (list-in (acl2::list-fix x) set) (list-in (double-rewrite y) set))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-take (implies (list-in (double-rewrite x) set) (iff (list-in (take n x) set) (or (in nil set) (<= (nfix n) (len x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-repeat (iff (list-in (acl2::repeat n x) set) (or (in x set) (zp n))) :rule-classes ((:rewrite)))
Theorem:
(defthm in-of-nth-when-list-in (implies (and (list-in x set) (< (nfix n) (len x))) (in (nth n x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-update-nth (implies (list-in (double-rewrite x) set) (iff (list-in (update-nth n y x) set) (and (in y set) (or (<= (nfix n) (len x)) (in nil set))))) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-butlast (implies (list-in (double-rewrite x) set) (list-in (butlast x n) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-nthcdr (implies (list-in (double-rewrite x) set) (list-in (nthcdr n x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-last (implies (list-in (double-rewrite x) set) (list-in (last x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-remove (implies (list-in x set) (list-in (remove a x) set)) :rule-classes ((:rewrite)))
Theorem:
(defthm list-in-of-revappend (equal (list-in (revappend x y) set) (and (list-in (acl2::list-fix x) set) (list-in y set))) :rule-classes ((:rewrite)))