Major Section: ACL2-BUILT-INS

Completion Axiom (`completion-of-<`

):

(equal (< x y) (if (and (rationalp x) (rationalp y)) (< x y) (let ((x1 (if (acl2-numberp x) x 0)) (y1 (if (acl2-numberp y) y 0))) (or (< (realpart x1) (realpart y1)) (and (equal (realpart x1) (realpart y1)) (< (imagpart x1) (imagpart y1)))))))

Guard for `(< x y)`

:

(and (rationalp x) (rationalp y))Notice that like all arithmetic functions,

`<`

treats non-numeric
inputs as `0`

.This function has the usual meaning on the rational numbers, but is extended to the complex rational numbers using the lexicographic order: first the real parts are compared, and if they are equal, then the imaginary parts are compared.