		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Nat-list-max

Signature
(nat-list-max x) → max
Arguments: x — Guard (nat-listp x).
Returns: max — Type (natp max).

Definitions and Theorems

Function: nat-list-max

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

Theorem: natp-of-nat-list-max

(defthm natp-of-nat-list-max
  (b* ((max (nat-list-max x))) (natp max))
  :rule-classes :type-prescription)

Theorem: nat-list-max-of-nat-list-fix-x

(defthm nat-list-max-of-nat-list-fix-x
  (equal (nat-list-max (acl2::nat-list-fix x))
         (nat-list-max x)))

Theorem: nat-list-max-nat-list-equiv-congruence-on-x

(defthm nat-list-max-nat-list-equiv-congruence-on-x
  (implies (acl2::nat-list-equiv x x-equiv)
           (equal (nat-list-max x)
                  (nat-list-max x-equiv)))
  :rule-classes :congruence)