		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Bst<-all-l

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

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

Definitions and Theorems

Function: bst<-all-l

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