CDR

returns the second element of a cons pair, else nil
Major Section:  PROGRAMMING

Completion Axiom:

(equal (cdr x)
       (cond
        ((consp x)
         (cdr x))
        (t nil)))

Guard:

(or (consp x) (equal x nil))
Notice that in the ACL2 logic, cdr returns nil for every atom.