		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Bst-p

Check the binary search tree property.

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

This recognizer is currently inefficient, operating in O(n^2) time instead of O(n). Eventually we hope to add an mbe with a linear-time executable version.

Definitions and Theorems

Function: bst-p

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