		Search-engine friendly clone of the ACL2 documentation.

Set-size

Set-size-theorems

Theorems about set-size.

Definitions and Theorems

Theorem: set-size-zero-empty

(defthm set-size-zero-empty
  (equal (equal (set-size-equal x) 0)
         (atom x)))

Theorem: set-size-of-true-list-fix

(defthm set-size-of-true-list-fix
  (equal (set-size-equal (true-list-fix x))
         (set-size-equal x)))

Theorem: set-size-of-cons

(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: set-size-of-add-to-set

(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: set-size-of-remove

(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: list-equiv-implies-equal-set-size-equal-1

(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: set-size-when-subsetp

(defthm set-size-when-subsetp
  (implies (subsetp-equal x y)
           (<= (set-size-equal x)
               (set-size-equal y))))

Theorem: set-size-when-subsetp-linear

(defthm set-size-when-subsetp-linear
  (implies (subsetp-equal x y)
           (<= (set-size-equal x)
               (set-size-equal y)))
  :rule-classes :linear)

Theorem: set-size-when-strict-subsetp

(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: set-size-when-strict-subsetp-linear

(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: set-size-when-set-equiv

(defthm set-size-when-set-equiv
  (implies (set-equiv x y)
           (equal (set-size-equal x)
                  (set-size-equal y))))

Theorem: set-size-when-set-equiv-linear

(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: set-equiv-implies-equal-set-size-equal-1

(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))

Subtopics

Set-size-lemmas: Lemmas useful to prove some of the theorems about set-size.