		Search-engine friendly clone of the ACL2 documentation.

Osets-of-natural-numbers

Nat-setp

Recognize finite sets of natural numbers.

Signature
(nat-setp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: nat-setp

(defun nat-setp (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'nat-setp))
    (declare (ignorable acl2::__function__))
    (and (setp x) (set-all-natp x))))

Theorem: booleanp-of-nat-setp

(defthm booleanp-of-nat-setp
  (acl2::b* ((yes/no (nat-setp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: setp-when-nat-setp

(defthm setp-when-nat-setp
  (implies (nat-setp nats) (setp nats)))

Theorem: nat-setp-of-insert

(defthm nat-setp-of-insert
  (equal (nat-setp (insert nat nats))
         (and (natp nat)
              (nat-setp (sfix nats)))))

Theorem: nat-setp-of-union

(defthm nat-setp-of-union
  (equal (nat-setp (union nats1 nats2))
         (and (nat-setp (sfix nats1))
              (nat-setp (sfix nats2)))))