		Search-engine friendly clone of the ACL2 documentation.

Left

Get the "left" subset of the nonempty set.

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

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 right subset. Concretely, it is the subset for which all elements are bst< the head. In terms of the underlying tree representation, this is the left subtree.

Definitions and Theorems

Function: left$inline

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

Theorem: setp-of-left

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