		Search-engine friendly clone of the ACL2 documentation.

Rotations

Rotate-left

Perform a left tree rotation.

Signature
(rotate-left tree) → tree$
Arguments: tree — Guard (binary-tree-p tree).
Returns: tree$ — Type (binary-tree-p tree$).

When the right subtree is empty (contrary to the guard), we logically just return the tree.

Definitions and Theorems

Function: rotate-left$inline

(defun rotate-left$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (declare (xargs :guard (not (tree-emptyp (tree-right tree)))))
  (if (mbt (not (tree-emptyp (tree-right tree))))
      (tree-node (tree-head (tree-right tree))
                 (tree-node (tree-head tree)
                            (tree-left tree)
                            (tree-left (tree-right tree)))
                 (tree-right (tree-right tree)))
    (tree-fix tree)))

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

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