		Search-engine friendly clone of the ACL2 documentation.

Right

Get the "right" subset of the nonempty set.

Signature
(right set) → right
Arguments: set — Guard (setp set).
Returns: right — Type (setp right).

For empty sets, returns nil.

From a user perspective, this should likely be viewed as an arbitrary proper subset excluding the head and disjoint from the left subset. Concretely, it is the subset for which the head is bst< all elements. In terms of the underlying tree representation, this is the right subtree.

Definitions and Theorems

Function: right$inline

(defun right$inline (set)
  (declare (xargs :guard (setp set)))
  (tree-right (sfix set)))

Theorem: setp-of-right

(defthm setp-of-right
  (b* ((right (right$inline set)))
    (setp right))
  :rule-classes :rewrite)