ACL2(r) recognizer for limited numbers
(I-limited x) is true if and only if x is a number that is not infinitely large. This predicate is only defined in ACL2(r) (see real).