		Search-engine friendly clone of the ACL2 documentation.

Obags

Tail

Rest of a non-empty obag after removing an occurrence of its smallest element.

Signature
(tail bag) → bag1
Arguments: bag — Guard (bagp bag).
Returns: bag1 — Type (bagp bag1).

This is similar to set::tail on osets.

Definitions and Theorems

Function: tail

(defun tail (bag)
       (declare (xargs :guard (bagp bag)))
       (declare (xargs :guard (not (empty bag))))
       (let ((__function__ 'tail))
            (declare (ignorable __function__))
            (mbe :logic (cdr (bfix bag))
                 :exec (cdr bag))))

Theorem: bagp-of-tail

(defthm bagp-of-tail
        (b* ((bag1 (tail bag))) (bagp bag1))
        :rule-classes :rewrite)

Theorem: tail-when-empty

(defthm tail-when-empty
        (implies (empty bag)
                 (equal (tail bag) nil))
        :rule-classes (:rewrite :type-prescription))

Theorem: tail-count

(defthm tail-count
        (implies (not (empty bag))
                 (< (acl2-count (tail bag))
                    (acl2-count bag)))
        :rule-classes (:rewrite :linear))

Theorem: tail-count-built-in

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