Definitions of the set-size functions and macros, and basic theorems about them.
Function:
(defun set-size-equal (x) (declare (xargs :guard (true-listp x))) (len (remove-duplicates-equal x)))
Function:
(defun set-size-eq-exec$guard-check (x) (declare (xargs :guard (symbol-listp x))) (declare (ignore x)) t)
Function:
(defun set-size-eq-exec (x) (declare (xargs :guard (symbol-listp x))) (len (remove-duplicates-eq x)))
Function:
(defun set-size-eql-exec$guard-check (x) (declare (xargs :guard (eqlable-listp x))) (declare (ignore x)) t)
Function:
(defun set-size-eql-exec (x) (declare (xargs :guard (eqlable-listp x))) (len (remove-duplicates x)))
Theorem:
(defthm set-size-eq-exec-is-set-size-equal (equal (set-size-eq-exec x) (set-size-equal x)))
Theorem:
(defthm set-size-eql-exec-is-set-size-equal (equal (set-size-eql-exec x) (set-size-equal x)))
Theorem:
(defthm natp-of-set-size-equal (natp (set-size-equal x)))
Theorem:
(defthm natp-of-set-size-eq-exec (natp (set-size-eq-exec x)))
Theorem:
(defthm natp-of-set-size-eql-exec (natp (set-size-eql-exec x)))