RTL generation in ACL2, starting step functions.