		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-union

Take the union of two treaps.

Signature
(tree-union x y) → tree
Arguments: x — Guard (binary-tree-p x).; y — Guard (binary-tree-p y).
Returns: tree — Type (binary-tree-p tree).

The result might not be a union if the input trees are not binary search trees.

Definitions and Theorems

Function: tree-union

(defun tree-union (x y)
  (declare (xargs :guard (and (binary-tree-p x)
                              (binary-tree-p y))))
  (let ((__function__ 'tree-union))
    (declare (ignorable __function__))
    (cond ((tree-emptyp x) (tree-fix y))
          ((tree-emptyp y) (tree-fix x))
          ((heap< (tree-head x) (tree-head y))
           (b* (((mv - left right)
                 (tree-split (tree-head y) x)))
             (tree-node (tree-head y)
                        (tree-union left (tree-left y))
                        (tree-union right (tree-right y)))))
          (t (b* (((mv - left right)
                   (tree-split (tree-head x) y)))
               (tree-node (tree-head x)
                          (tree-union (tree-left x) left)
                          (tree-union (tree-right x) right)))))))

Theorem: binary-tree-p-of-tree-union

(defthm binary-tree-p-of-tree-union
  (b* ((tree (tree-union x y)))
    (binary-tree-p tree))
  :rule-classes :rewrite)