Very basic lemmas about subsetp.
Theorem:
(defthm subsetp-when-atom-left (implies (atom x) (subsetp x y)))
Theorem:
(defthm subsetp-when-atom-right (implies (atom y) (equal (subsetp x y) (atom x))))
Theorem:
(defthm subsetp-nil (subsetp nil x))
Theorem:
(defthm subsetp-of-cons (equal (subsetp (cons a x) y) (if (member a y) (subsetp x y) nil)))
Theorem:
(defthm subsetp-member (implies (and (member a x) (subsetp x y)) (member a y)) :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (subsetp x y) (member a x)) (member a y))) (:rewrite :corollary (implies (and (not (member a y)) (subsetp x y)) (not (member a x)))) (:rewrite :corollary (implies (and (subsetp x y) (not (member a y))) (not (member a x))))))
Theorem:
(defthm element-list-p-when-subsetp-equal-true-list (implies (and (subsetp-equal x y) (element-list-p y) (not (element-list-final-cdr-p t))) (equal (element-list-p x) (true-listp x))) :rule-classes :rewrite)
Theorem:
(defthm element-list-p-when-subsetp-equal-non-true-list (implies (and (subsetp-equal x y) (element-list-p y) (element-list-final-cdr-p t)) (element-list-p x)) :rule-classes :rewrite)
Theorem:
(defthm subsetp-of-elementlist-projection-when-subsetp (implies (subsetp x y) (subsetp (elementlist-projection x) (elementlist-projection y))) :rule-classes :rewrite)
Theorem:
(defthm subsetp-refl (subsetp x x))
Theorem:
(defthm subsetp-trans (implies (and (subsetp x y) (subsetp y z)) (subsetp x z)))
Theorem:
(defthm subsetp-trans2 (implies (and (subsetp y z) (subsetp x y)) (subsetp x z)))
Theorem:
(defthm subsetp-implies-subsetp-cdr (implies (subsetp x y) (subsetp (cdr x) y)))
Theorem:
(defthm subsetp-of-cdr (subsetp (cdr x) x))
Theorem:
(defthm subsetp-cons-same (implies (subsetp a b) (subsetp (cons x a) (cons x b))))
Theorem:
(defthm subsetp-cons-2 (implies (subsetp a b) (subsetp a (cons x b))))
Theorem:
(defthm subsetp-append1 (equal (subsetp (append a b) c) (and (subsetp a c) (subsetp b c))))
Theorem:
(defthm subsetp-append2 (subsetp a (append a b)))
Theorem:
(defthm subsetp-append3 (subsetp b (append a b)))
Theorem:
(defthm subsetp-of-append-when-subset-of-either (implies (or (subsetp a b) (subsetp a c)) (subsetp a (append b c))))
Theorem:
(defthm subsetp-car-member (implies (and (subsetp x y) (consp x)) (member (car x) y)))
Theorem:
(defthm subsetp-intersection-equal (iff (subsetp a (intersection-equal b c)) (and (subsetp a b) (subsetp a c))))
Theorem:
(defthm subsetp-of-elementlist-mapappend-when-subsetp (implies (subsetp x y) (subsetp (elementlist-mapappend x) (elementlist-mapappend y))) :rule-classes :rewrite)
Theorem:
(defthm set-equiv-congruence-over-elementlist-mapappend (implies (set-equiv x y) (set-equiv (elementlist-mapappend x) (elementlist-mapappend y))) :rule-classes :congruence)