		Search-engine friendly clone of the ACL2 documentation.

Utilities

Max-nats

Maximum member in a list of naturals.

Signature
(max-nats x) → *
Arguments: x — Guard (nat-listp x).

Typically you would only use this on non-empty lists, but as a reasonable default we say the maximum member of the empty list is 0.

Definitions and Theorems

Function: max-nats

(defun max-nats (x)
  (declare (xargs :guard (nat-listp x)))
  (let ((__function__ 'max-nats))
    (declare (ignorable __function__))
    (if (atom x)
        0
      (max (lnfix (car x))
           (max-nats (cdr x))))))

Theorem: max-nats-when-atom

(defthm max-nats-when-atom
  (implies (atom x)
           (equal (max-nats x) 0)))

Theorem: max-nats-of-cons

(defthm max-nats-of-cons
  (equal (max-nats (cons a x))
         (max (nfix a) (max-nats x))))

Theorem: natp-of-max-nats

(defthm natp-of-max-nats
  (natp (max-nats x))
  :rule-classes :type-prescription)

Theorem: max-nats-of-append

(defthm max-nats-of-append
  (equal (max-nats (append x y))
         (max (max-nats x) (max-nats y))))

Theorem: max-nats-of-rev

(defthm max-nats-of-rev
  (equal (max-nats (rev x)) (max-nats x)))

Theorem: max-nats-of-revappend

(defthm max-nats-of-revappend
  (equal (max-nats (revappend x y))
         (max (max-nats x) (max-nats y))))