		Search-engine friendly clone of the ACL2 documentation.

Tree-left

Get the left subtree of the nonempty binary-tree.

For empty trees, returns nil.

Function: tree-left$inline

(defun tree-left$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (cadr (tree-fix tree)))

Theorem: binary-tree-p-of-tree-left

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