# Setp

`(setp x)` recognizes well-formed ordered sets.

A proper ordered set is a true-listp whose elements are
fully ordered under <<. Note that this implicitly means that sets have
no duplicate elements.

Testing setp is necessarily somewhat slow: we have to check that the
elements are in order. Its cost is linear in the size of n.

### Definitions and Theorems

**Function: **setp

(defun setp (x)
(declare (xargs :guard t))
(if (atom x)
(null x)
(or (null (cdr x))
(and (consp (cdr x))
(fast-<< (car x) (cadr x))
(setp (cdr x))))))

**Theorem: **setp-type

(defthm setp-type
(or (equal (setp x) t)
(equal (setp x) nil))
:rule-classes :type-prescription)

**Theorem: **sets-are-true-lists

(defthm sets-are-true-lists
(implies (setp x) (true-listp x)))

**Theorem: **sets-are-true-lists-compound-recognizer

(defthm sets-are-true-lists-compound-recognizer
(implies (setp x) (true-listp x))
:rule-classes :compound-recognizer)

**Theorem: **sets-are-true-lists-cheap

(defthm sets-are-true-lists-cheap
(implies (setp x) (true-listp x))
:rule-classes ((:rewrite :backchain-limit-lst (1))))