Theorems about set-size.
Theorem:
(defthm set-size-zero-empty (equal (equal (set-size-equal x) 0) (atom x)))
Theorem:
(defthm set-size-of-true-list-fix (equal (set-size-equal (true-list-fix x)) (set-size-equal x)))
Theorem:
(defthm set-size-of-cons (equal (set-size-equal (cons a x)) (if (member-equal a x) (set-size-equal x) (1+ (set-size-equal x)))))
Theorem:
(defthm set-size-of-add-to-set (equal (set-size-equal (add-to-set-equal a x)) (if (member-equal a x) (set-size-equal x) (1+ (set-size-equal x)))))
Theorem:
(defthm set-size-of-remove (equal (set-size-equal (remove-equal a x)) (if (member-equal a x) (1- (set-size-equal x)) (set-size-equal x))))
Theorem:
(defthm list-equiv-implies-equal-set-size-equal-1 (implies (list-equiv x x-equiv) (equal (set-size-equal x) (set-size-equal x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm set-size-when-subsetp (implies (subsetp-equal x y) (<= (set-size-equal x) (set-size-equal y))))
Theorem:
(defthm set-size-when-subsetp-linear (implies (subsetp-equal x y) (<= (set-size-equal x) (set-size-equal y))) :rule-classes :linear)
Theorem:
(defthm set-size-when-strict-subsetp (implies (and (subsetp-equal x y) (not (subsetp-equal y x))) (< (set-size-equal x) (set-size-equal y))))
Theorem:
(defthm set-size-when-strict-subsetp-linear (implies (and (subsetp-equal x y) (not (subsetp-equal y x))) (< (set-size-equal x) (set-size-equal y))) :rule-classes :linear)
Theorem:
(defthm set-size-when-set-equiv (implies (set-equiv x y) (equal (set-size-equal x) (set-size-equal y))))
Theorem:
(defthm set-size-when-set-equiv-linear (implies (set-equiv x y) (equal (set-size-equal x) (set-size-equal y))) :rule-classes :linear)
Theorem:
(defthm set-equiv-implies-equal-set-size-equal-1 (implies (set-equiv x x-equiv) (equal (set-size-equal x) (set-size-equal x-equiv))) :rule-classes (:congruence))