`(cardinality x)` computes the number of elements in

This is like length, but respects the non-set convention and always returns 0 for ill-formed sets.

**Function: **

(defun cardinality (x) (declare (xargs :guard (setp x))) (mbe :logic (if (empty x) 0 (1+ (cardinality (tail x)))) :exec (length (the list x))))

**Theorem: **

(defthm cardinality-type (and (integerp (cardinality x)) (<= 0 (cardinality x))) :rule-classes :type-prescription)

**Theorem: **

(defthm cardinality-zero-empty (equal (equal (cardinality x) 0) (empty x)))

**Theorem: **

(defthm cardinality-sfix-cancel (equal (cardinality (sfix x)) (cardinality x)))

**Theorem: **

(defthm insert-cardinality (equal (cardinality (insert a x)) (if (in a x) (cardinality x) (1+ (cardinality x)))))

**Theorem: **

(defthm delete-cardinality (equal (cardinality (delete a x)) (if (in a x) (1- (cardinality x)) (cardinality x))))

**Theorem: **

(defthm subset-cardinality (implies (subset x y) (<= (cardinality x) (cardinality y))) :rule-classes (:rewrite :linear))

**Theorem: **

(defthm equal-cardinality-subset-is-equality (implies (and (setp x) (setp y) (subset x y) (equal (cardinality x) (cardinality y))) (equal (equal x y) t)))

**Theorem: **

(defthm proper-subset-cardinality (implies (and (subset x y) (not (subset y x))) (< (cardinality x) (cardinality y))) :rule-classes (:rewrite :linear))