		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)