		Search-engine friendly clone of the ACL2 documentation.

Candidates-with-min-votes

Min-nats

Pick the minimum number in a list of natural numbers

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

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
  (implies (and (nat-listp x))
           (b* ((min (min-nats x))) (natp min)))
  :rule-classes (:rewrite :type-prescription))

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

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