		Search-engine friendly clone of the ACL2 documentation.

Utilities

Min-nats

Minimum member in a list of naturals.

Signature
(min-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 minimum of the empty list is 0.

Definitions and Theorems

Function: min-nats

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

Theorem: natp-of-min-nats

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

Theorem: min-nats-bound

(defthm min-nats-bound
  (implies (consp x)
           (<= (min-nats x) (max-nats x)))
  :rule-classes ((:rewrite) (:linear)))