		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 (emptyp 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-emptyp

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

Theorem: tail-count

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

Theorem: tail-count-built-in

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

Theorem: head-tail-order

(defthm head-tail-order
  (implies (not (emptyp (tail x)))
           (<< (mv-nth 0 (head x))
               (mv-nth 0 (head (tail x))))))

Theorem: head-tail-order-contrapositive

(defthm head-tail-order-contrapositive
  (implies (not (<< (mv-nth 0 (head x))
                    (mv-nth 0 (head (tail x)))))
           (emptyp (tail x))))

Theorem: tail-of-mfix-map

(defthm tail-of-mfix-map
  (equal (tail (mfix map)) (tail map)))

Theorem: tail-mequiv-congruence-on-map

(defthm tail-mequiv-congruence-on-map
  (implies (mequiv map map-equiv)
           (equal (tail map) (tail map-equiv)))
  :rule-classes :congruence)