		Search-engine friendly clone of the ACL2 documentation.

Tree-right

Get the right subtree of the nonempty binary-tree.

For empty trees, returns nil.

Function: tree-right$inline

(defun tree-right$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (cddr (tree-fix tree)))

Theorem: binary-tree-p-of-tree-right

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