		Search-engine friendly clone of the ACL2 documentation.

In

Determine if a value is a member of the set.

Signature
(in x set) → *
Arguments: set — Guard (setp set).

Time complexity: O(log(n)).

Definitions and Theorems

Function: in

(defun in (x set)
  (declare (xargs :guard (setp set)))
  (declare (xargs :type-prescription (booleanp (in x set))))
  (let ((__function__ 'in))
    (declare (ignorable __function__))
    (mbe :logic (tree-in x (sfix set))
         :exec (and (not (emptyp set))
                    (or (equal x (head set))
                        (if (bst< x (head set))
                            (in x (left set))
                          (in x (right set))))))))

Theorem: tree-in-of-sfix-becomes-in-exec

(defthm tree-in-of-sfix-becomes-in-exec
  (equal (tree-in x (sfix set))
         (and (not (emptyp set))
              (or (equal x (head set))
                  (if (bst< x (head set))
                      (in x (left set))
                    (in x (right set)))))))