		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Bst<-all-r

Check that some value is bst< all members of a tree.

Signature
(bst<-all-r x tree) → *
Arguments: tree — Guard (binary-tree-p tree).

Definitions and Theorems

Function: bst<-all-r

(defun bst<-all-r (x tree)
 (declare (xargs :guard (binary-tree-p tree)))
 (declare (xargs :type-prescription (booleanp (bst<-all-r x tree))))
 (let ((__function__ 'bst<-all-r))
   (declare (ignorable __function__))
   (or (tree-emptyp tree)
       (and (bst< x (tree-head tree))
            (bst<-all-r x (tree-left tree))
            (bst<-all-r x (tree-right tree))))))