		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-intersect

Take the intersection of two treaps.

Signature
(tree-intersect 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 intersection if the input trees are not binary search trees.

Definitions and Theorems

Function: tree-intersect

(defun tree-intersect (x y)
 (declare (xargs :guard (and (binary-tree-p x)
                             (binary-tree-p y))))
 (declare
   (xargs :type-prescription (or (consp (tree-intersect x y))
                                 (equal (tree-intersect x y) nil))))
 (let ((__function__ 'tree-intersect))
   (declare (ignorable __function__))
   (cond ((or (tree-emptyp x) (tree-emptyp y))
          nil)
         ((heap< (tree-head x) (tree-head y))
          (b* (((mv in left right)
                (tree-split (tree-head y) x))
               (left (tree-intersect left (tree-left y)))
               (right (tree-intersect right (tree-right y))))
            (if in (tree-node (tree-head y) left right)
              (tree-join-at (tree-head y)
                            left right))))
         (t (b* (((mv in left right)
                  (tree-split (tree-head x) y))
                 (left (tree-intersect (tree-left x) left))
                 (right (tree-intersect (tree-right x) right)))
              (if in (tree-node (tree-head x) left right)
                (tree-join-at (tree-head x)
                              left right)))))))

Theorem: binary-tree-p-of-tree-intersect

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