The last cdr of a list
(Last-cdr x) is x if x is an atom, and
otherwise is the last cdr of a list. Here are examples.
ACL2 !>(last-cdr '(a b . c))
ACL2 !>(last-cdr '(a b c))
(Last-cdr x) has a guard of t.
(defun last-cdr (x)
(declare (xargs :guard t))
(if (atom x) x (cdr (last x))))