		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Heapp

Check the max heap property.

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

Definitions and Theorems

Function: heapp

(defun heapp (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (declare (xargs :type-prescription (booleanp (heapp tree))))
  (let ((__function__ 'heapp))
    (declare (ignorable __function__))
    (or (tree-emptyp tree)
        (mbe :logic
             (and (heapp (tree-left tree))
                  (heapp (tree-right tree))
                  (heap<-all-l (tree-left tree)
                               (tree-head tree))
                  (heap<-all-l (tree-right tree)
                               (tree-head tree)))
             :exec
             (b* (((mv heapp -)
                   (fast-nonempty-heapp tree)))
               heapp)))))