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