An alternate well-founded-relation that allows lists of naturals to be used directly as measures.

This is essentially syntactic sugar for nat-list-measure.
We introduce

(defun f (a b c) (declare (xargs :measure (nat-list-measure (list a b c)))) ...)

You can instead write:

(defun f (a b c) (declare (xargs :measure (list a b c) :well-founded-relation nat-list-<)) ...)

That's more verbose in this example, but in practice it can often end up being more concise. In particular:

- You can use set-well-founded-relation to install
nat-list-< as your well-founded relation ahead of time. - In a big mutual-recursion, you only need to give the
:well-founded-relation to a single definition.

**Function: **

(defun nat-list-< (a b) (o< (nat-list-measure a) (nat-list-measure b)))

**Theorem: **

(defthm nat-list-wfr (and (o-p (nat-list-measure x)) (implies (nat-list-< x y) (o< (nat-list-measure x) (nat-list-measure y)))) :rule-classes :well-founded-relation)

**Theorem: **

(defthm open-nat-list-< (implies (syntaxp (and (cons-list-or-quotep a) (cons-list-or-quotep b))) (equal (nat-list-< a b) (or (< (len a) (len b)) (and (equal (len a) (len b)) (if (consp a) (or (< (nfix (car a)) (nfix (car b))) (and (equal (nfix (car a)) (nfix (car b))) (nat-list-< (cdr a) (cdr b)))) (< (nfix a) (nfix b))))))))

**Theorem: **

(defthm natp-nat-list-< (implies (and (atom a) (atom b)) (equal (nat-list-< a b) (< (nfix a) (nfix b)))))