		Search-engine friendly clone of the ACL2 documentation.

<

Less-than

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. Thus, the following are theorems.

(thm (equal (< (fix x) y) (< x y)))
(thm (equal (< x (fix y)) (< x y)))

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.