		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-in

Determine if a value appears in the tree.

Signature
(tree-in x tree) → *
Arguments: tree — Guard (binary-tree-p tree).

No assumptions are made about the structure of the tree, so this search takes linear time. In practice, this function is only used as part of the logical definition of in (which is provided a more efficient implementation with mbe).

Definitions and Theorems

Function: tree-in

(defun tree-in (x tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (declare (xargs :type-prescription (booleanp (tree-in x tree))))
  (let ((__function__ 'tree-in))
    (declare (ignorable __function__))
    (and (not (tree-emptyp tree))
         (or (equal x (tree-head tree))
             (tree-in x (tree-left tree))
             (tree-in x (tree-right tree))))))