Modular Arithmetic : Background Cannot simply declare Common Lisp + operator as 32 bits The result of adding two 32-bit numbers is 33 bits Implies that the guard condition is generally unsatisfiable GCL normally recognizes only the symbol "+" as addition Cannot provide a logical replacement for + in ACL2 No efficient implementation of 32-bit addition in ACL2