# Two-nats-measure

An ordinal measure for admitting functions: lexicographic ordering of
two natural numbers.

`(two-nats-measure a b)` constructs an ordinal that can be used
to prove that recursive functions terminate. It essentially provides a
lexicographic order where a is more significant than b. More
precisely, its correctness is understood through the theorem:

**Theorem: **o<-of-two-nats-measure

(defthm o<-of-two-nats-measure
(equal (o< (two-nats-measure a b)
(two-nats-measure c d))
(or (< (nfix a) (nfix c))
(and (equal (nfix a) (nfix c))
(< (nfix b) (nfix d))))))

This is often useful for admitting mutually recursive functions where
one function inspects its argument and then immediately calls another.
For instance, suppose you want to admit:

(mutual-recursion
(defun f (x) ...)
(defun g (x) (if (special-p x) (f x) ...)))

Then since g calls f on the same argument, you can't just use
ACL2-count, or for that matter any other measure that only considers
the argument x) to show that the call of (f x) has made progress.
However, it's easy to use two-nats-measure to ``rank'' the functions
so that f is always considered smaller than g:

(mutual-recursion
(defun f (x)
(declare (xargs :measure (two-nats-measure (acl2-count x) 0)))
...)
(defun g (x)
(declare (xargs :measure (two-nats-measure (acl2-count x) 1)))
...))

More generally two-nats-measure may be useful whenever you want to
admit an algorithm that makes different kinds of progress.

Example. Suppose you have a pile of red socks and a pile of blue socks to
put away. Every time you put away a red sock, I add a bunch of blue socks to
your pile, but when you put a blue sock away, I don't get to add any more
socks. You will eventually finish since the pile never gets any new red
socks. You can admit a function like this with (two-nats-measure num-red
num-blue).

See also nat-list-measure for a generalization of this to a
lexicographic ordering of a list of natural numbers (of any length instead of
just two numbers).

### Definitions and Theorems

**Function: **two-nats-measure

(defun two-nats-measure (a b)
(declare (xargs :guard (and (natp a) (natp b))))
(make-ord 2 (+ 1 (nfix a))
(make-ord 1 (+ 1 (nfix b)) 0)))

**Theorem: **o-p-of-two-nats-measure

(defthm o-p-of-two-nats-measure
(equal (o-p (two-nats-measure a b)) t))

**Theorem: **o<-of-two-nats-measure

(defthm o<-of-two-nats-measure
(equal (o< (two-nats-measure a b)
(two-nats-measure c d))
(or (< (nfix a) (nfix c))
(and (equal (nfix a) (nfix c))
(< (nfix b) (nfix d))))))