		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-join-at

Wrapper around tree-join annotated with a split point.

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

This split argument is the value such that:

(and (bst<-all-l left split)
     (bst<-all-r split right))

While the split argument is not used by the function, it is convenient to have so various rewriting rules can bind the variable appropriately without requiring :use hints.

Definitions and Theorems

Function: tree-join-at$inline

(defun tree-join-at$inline (split left right)
  (declare (xargs :guard (and (binary-tree-p left)
                              (binary-tree-p right))))
  (declare (ignore split))
  (tree-join left right))

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

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