		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-diff

Take the difference of two treaps.

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

Definitions and Theorems

Function: tree-diff

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

Theorem: binary-tree-p-of-tree-diff

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