		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Heap<-all-l

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

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

Definitions and Theorems

Function: heap<-all-l

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