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.