• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Std/lists/add-to-set
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/lists

Final-cdr

(final-cdr x) returns the atom in the "cdr-most branch" of x.

For example, (final-cdr '(a b c . d)) is d.

This function is related to list-fix. It is occasionally useful for strengthening rewrite rules by removing hypotheses.

Definitions and Theorems

Function: final-cdr

(defun final-cdr (x)
  (declare (xargs :guard t))
  (if (atom x) x (final-cdr (cdr x))))

Theorem: final-cdr-when-atom

(defthm final-cdr-when-atom
  (implies (atom x)
           (equal (final-cdr x) x)))

Theorem: final-cdr-of-cons

(defthm final-cdr-of-cons
  (equal (final-cdr (cons a x))
         (final-cdr x)))

Theorem: final-cdr-when-true-listp

(defthm final-cdr-when-true-listp
  (implies (true-listp x)
           (equal (final-cdr x) nil)))

Theorem: equal-final-cdr-nil

(defthm equal-final-cdr-nil
  (equal (equal (final-cdr x) nil)
         (true-listp x)))

Theorem: equal-of-final-cdr-and-self

(defthm equal-of-final-cdr-and-self
  (equal (equal x (final-cdr x))
         (atom x)))

Theorem: final-cdr-of-append

(defthm final-cdr-of-append
  (equal (final-cdr (append x y))
         (final-cdr y)))

Theorem: final-cdr-of-revappend

(defthm final-cdr-of-revappend
  (equal (final-cdr (revappend x y))
         (final-cdr y)))

Theorem: final-cdr-of-union-equal

(defthm final-cdr-of-union-equal
  (equal (final-cdr (union-equal x y))
         (final-cdr y)))

Theorem: final-cdr-of-acons

(defthm final-cdr-of-acons
  (equal (final-cdr (acons key val alist))
         (final-cdr alist)))

Theorem: final-cdr-of-hons-acons

(defthm final-cdr-of-hons-acons
  (equal (final-cdr (hons-acons key val alist))
         (final-cdr alist)))

Theorem: final-cdr-of-hons-shrink-alist

(defthm final-cdr-of-hons-shrink-alist
  (equal (final-cdr (hons-shrink-alist alist ans))
         (final-cdr ans)))

Theorem: final-cdr-of-add-to-set-equal

(defthm final-cdr-of-add-to-set-equal
  (equal (final-cdr (add-to-set-equal a x))
         (final-cdr x)))

Theorem: final-cdr-of-last

(defthm final-cdr-of-last
  (equal (final-cdr (last x))
         (final-cdr x)))

Theorem: final-cdr-of-nthcdr

(defthm final-cdr-of-nthcdr
  (equal (final-cdr (nthcdr n x))
         (if (<= (nfix n) (len x))
             (final-cdr x)
           nil)))

Theorem: append-self-onto-final-cdr

(defthm append-self-onto-final-cdr
  (equal (append x (final-cdr x)) x))