		Search-engine friendly clone of the ACL2 documentation.

Std/lists/last

Lemmas about last available in the std/lists library.

Definitions and Theorems

Theorem: last-when-atom

(defthm last-when-atom
        (implies (atom x) (equal (last x) x)))

Theorem: last-when-atom-of-cdr

(defthm last-when-atom-of-cdr
        (implies (atom (cdr x))
                 (equal (last x) x)))

Theorem: last-of-cons

(defthm last-of-cons
        (equal (last (cons a x))
               (if (consp x) (last x) (cons a x))))

Theorem: consp-of-last

(defthm consp-of-last
        (equal (consp (last l)) (consp l)))

Theorem: true-listp-of-last

(defthm true-listp-of-last
        (equal (true-listp (last l))
               (true-listp l)))

Theorem: len-of-last

(defthm len-of-last
        (equal (len (last l))
               (if (consp l) 1 0)))

Theorem: upper-bound-of-len-of-last

(defthm upper-bound-of-len-of-last
        (< (len (last x)) 2)
        :rule-classes :linear)

Theorem: member-of-car-of-last

(defthm member-of-car-of-last
        (iff (member (car (last x)) x)
             (if (consp x) t nil)))

Theorem: subsetp-of-last

(defthm subsetp-of-last (subsetp (last x) x))

Theorem: last-of-append

(defthm last-of-append
        (equal (last (append x y))
               (if (consp y)
                   (last y)
                   (append (last x) y))))

Theorem: last-of-rev

(defthm last-of-rev
        (equal (last (rev x))
               (if (consp x) (list (car x)) nil)))

Theorem: last-of-revappend

(defthm last-of-revappend
        (equal (last (revappend x y))
               (cond ((consp y) (last y))
                     ((consp x) (cons (car x) y))
                     (t y))))

Theorem: element-list-p-of-last

(defthm element-list-p-of-last
        (implies (element-list-p (double-rewrite x))
                 (element-list-p (last x)))
        :rule-classes :rewrite)