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:
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)))))