		Search-engine friendly clone of the ACL2 documentation.

L<

Ordering on naturals or lists of naturals

The function l< is a straightforward ordering relation that compares two objects, each of which is a natural number or a list of natural numbers. It may be convenient to apply lex-fix to two objects before comparing them with l<. Below are the relevant definitions.

Function: l<

(defun l< (x y)
  (declare (xargs :guard (and (lexp x) (lexp y))))
  (or (< (len x) (len y))
      (and (= (len x) (len y))
           (if (atom x) (< x y) (d< x y)))))

Function: lexp

(defun lexp (x)
  (declare (xargs :guard t))
  (or (natp x)
      (and (consp x) (nat-listp x))))

Function: d<

(defun d< (x y)
  (declare (xargs :guard (and (nat-listp x) (nat-listp y))))
  (and (consp x)
       (consp y)
       (or (< (car x) (car y))
           (and (= (car x) (car y))
                (d< (cdr x) (cdr y))))))

Function: lex-fix

(defun lex-fix (x)
  (declare (xargs :guard t))
  (cond ((atom x) (nfix x))
        (t (nfix-list x))))

Function: nfix-list

(defun nfix-list (list)
  (declare (xargs :guard t))
  (if (consp list)
      (cons (nfix (car list))
            (nfix-list (cdr list)))
    nil))