		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-join

Join two trees which have previously been tree-split.

Signature
(tree-join left right) → tree
Arguments: left — Guard (binary-tree-p left).; right — Guard (binary-tree-p right).
Returns: tree — Type (binary-tree-p tree).

Technically it is not required that the two trees are a result of a previous split call. It is only expected that, given a join (tree-join left right), there exists some x such that (bst<-all-l left x) and (bst<-all-r x right), as is produced by split.

Definitions and Theorems

Function: tree-join

(defun tree-join (left right)
  (declare (xargs :guard (and (binary-tree-p left)
                              (binary-tree-p right))))
  (let ((__function__ 'tree-join))
    (declare (ignorable __function__))
    (cond ((tree-emptyp left) (tree-fix right))
          ((tree-emptyp right) (tree-fix left))
          ((heap< (tree-head left)
                  (tree-head right))
           (tree-node (tree-head right)
                      (tree-join left (tree-left right))
                      (tree-right right)))
          (t (tree-node (tree-head left)
                        (tree-left left)
                        (tree-join (tree-right left) right))))))

Theorem: binary-tree-p-of-tree-join

(defthm binary-tree-p-of-tree-join
  (b* ((tree (tree-join left right)))
    (binary-tree-p tree))
  :rule-classes :rewrite)