		Search-engine friendly clone of the ACL2 documentation.

First-choice-of-majority-p

Max-nats

Pick the maximum number in a list of natural numbers

Signature
(max-nats x) → max
Arguments: x — Guard (nat-listp x).
Returns: max — Type (natp max), given the guard.

Definitions and Theorems

Function: max-nats

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

Theorem: natp-of-max-nats

(defthm natp-of-max-nats
  (implies (and (nat-listp x))
           (b* ((max (max-nats x))) (natp max)))
  :rule-classes (:rewrite :type-prescription))

Theorem: max-nats-returns-a-member-of-input

(defthm max-nats-returns-a-member-of-input
  (implies (and (nat-listp x) (consp x))
           (member-equal (max-nats x) x)))

Theorem: max-nats-of-list-of-one-element

(defthm max-nats-of-list-of-one-element
  (implies (natp e)
           (equal (max-nats (list e)) e)))

Theorem: max-nats-and-cons

(defthm max-nats-and-cons
  (<= (max-nats x) (max-nats (cons e x)))
  :rule-classes :linear)

Theorem: max-nats-is-greater-than-any-other-list-element

(defthm max-nats-is-greater-than-any-other-list-element
  (implies (and (member-equal e x)
                (not (equal e (max-nats x)))
                (nat-listp x))
           (< e (max-nats x)))
  :rule-classes :linear)