		Search-engine friendly clone of the ACL2 documentation.

Primitives

Head

(head x) returns the smallest element in a set.

This is like car, but respects the non-set convention and always returns nil for ill-formed sets.

Definitions and Theorems

Function: head

(defun head (x)
       (declare (xargs :guard (and (setp x) (not (empty x)))))
       (mbe :logic (car (sfix x))
            :exec (car x)))

Theorem: head-count

(defthm head-count
        (implies (not (empty x))
                 (< (acl2-count (head x))
                    (acl2-count x)))
        :rule-classes ((:rewrite) (:linear)))

Theorem: head-count-built-in

(defthm head-count-built-in
        (implies (not (empty x))
                 (o< (acl2-count (head x))
                     (acl2-count x)))
        :rule-classes :built-in-clause)

Theorem: head-when-empty

(defthm head-when-empty
        (implies (empty x)
                 (equal (head x) nil)))

Theorem: head-sfix-cancel

(defthm head-sfix-cancel
        (equal (head (sfix x)) (head x)))

Theorem: head-minimal

(defthm head-minimal
        (implies (<< a (head x))
                 (not (in a x))))

Theorem: head-minimal-2

(defthm head-minimal-2
        (implies (in a x)
                 (not (<< a (head x)))))

Theorem: head-unique

(defthm head-unique
        (not (in (head x) (tail x))))