Is every number in a list smaller than some maximum?
Function:
(defun nats-below-p (max x) (declare (xargs :guard (and (natp max) (nat-listp x)))) (let ((__function__ 'nats-below-p)) (declare (ignorable __function__)) (if (atom x) t (and (< (car x) max) (nats-below-p max (cdr x))))))