		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-delete

Remove a value from the tree.

Signature
(tree-delete x tree) → tree$
Arguments: tree — Guard (binary-tree-p tree).
Returns: tree$ — Type (binary-tree-p tree$).

The tree is expected to be a binary search tree. If it is not, the element x intended to be deleted might outside the search path and thus remain in the tree.

After deletion, the tree is rebalanced with respect to the heapp property.

Definitions and Theorems

Function: tree-delete

(defun tree-delete (x tree)
 (declare (xargs :guard (binary-tree-p tree)))
 (declare
   (xargs :type-prescription (or (consp (tree-delete x tree))
                                 (equal (tree-delete x tree) nil))))
 (let ((__function__ 'tree-delete))
   (declare (ignorable __function__))
   (b* (((when (tree-emptyp tree)) nil)
        ((when (equal x (tree-head tree)))
         (cond ((tree-emptyp (tree-left tree))
                (tree-right tree))
               ((tree-emptyp (tree-right tree))
                (tree-left tree))
               (t (tree-join-at (tree-head tree)
                                (tree-left tree)
                                (tree-right tree))))))
     (if (bst< x (tree-head tree))
         (tree-node-with-hint (tree-head tree)
                              (tree-delete x (tree-left tree))
                              (tree-right tree)
                              tree)
       (tree-node-with-hint (tree-head tree)
                            (tree-left tree)
                            (tree-delete x (tree-right tree))
                            tree)))))

Theorem: binary-tree-p-of-tree-delete

(defthm binary-tree-p-of-tree-delete
  (b* ((tree$ (tree-delete x tree)))
    (binary-tree-p tree$))
  :rule-classes :rewrite)