Very basic lemmas about member.
Theorem:
(defthm member-when-atom (implies (atom x) (not (member a x))))
Theorem:
(defthm member-of-cons (equal (member a (cons b x)) (if (equal a b) (cons b x) (member a x))))
Theorem:
(defthm member-of-car (equal (member (car x) x) (if (consp x) x nil)))
Theorem:
(defthm member-of-append (iff (member a (append x y)) (or (member a x) (member a y))))
Theorem:
(defthm member-of-set-difference-equal (iff (member a (set-difference-equal x y)) (and (member a x) (not (member a y)))))
Theorem:
(defthm member-of-intersection-equal (iff (member a (intersection-equal x y)) (and (member a x) (member a y))))
Theorem:
(defthm member-of-remove (iff (member a (remove b x)) (and (member a x) (not (equal a b)))))
Theorem:
(defthm acl2-count-when-member (implies (member a x) (< (acl2-count a) (acl2-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm member-self (not (member x x)))
Theorem:
(defthm element-p-when-member-equal-of-element-list-not-negated (and (implies (and (member-equal a x) (element-list-p x)) (element-p a)) (implies (and (element-list-p x) (member-equal a x)) (element-p a))) :rule-classes :rewrite)
Theorem:
(defthm element-p-when-member-equal-of-element-list-negated (and (implies (and (member-equal a x) (element-list-p x)) (not (non-element-p a))) (implies (and (element-list-p x) (member-equal a x)) (not (non-element-p a)))) :rule-classes :rewrite)
Theorem:
(defthm member-of-element-xformer-in-elementlist-projection (implies (member k x) (member (element-xformer k) (elementlist-projection x))) :rule-classes :rewrite)
Theorem:
(defthm member-in-elementlist-mapappend (implies (and (member k (element-listxformer j)) (member j x)) (member k (elementlist-mapappend x))) :rule-classes :rewrite)