		Search-engine friendly clone of the ACL2 documentation.

Omaps

Tail

Rest of a non-empty omap after removing its smallest pair.

Signature
(tail map) → map1
Arguments: map — Guard (mapp map).
Returns: map1 — Type (mapp map1).

This is similar to set::tail for osets.

Definitions and Theorems

Function: tail

(defun tail (map)
  (declare (xargs :guard (mapp map)))
  (declare (xargs :guard (not (empty map))))
  (let ((__function__ 'tail))
    (declare (ignorable __function__))
    (cdr (mfix map))))

Theorem: mapp-of-tail

(defthm mapp-of-tail
  (b* ((map1 (tail map))) (mapp map1))
  :rule-classes :rewrite)

Theorem: tail-when-empty

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

Theorem: tail-count

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

Theorem: tail-count-built-in

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