		Search-engine friendly clone of the ACL2 documentation.

Addresses

All-addresses-valid?

Signature
(all-addresses-valid? addresses) → y/n
Arguments: addresses — Guard (address-listp addresses).
Returns: y/n — Type (booleanp y/n).

Definitions and Theorems

Function: all-addresses-valid?

(defun all-addresses-valid? (addresses)
  (declare (xargs :guard (address-listp addresses)))
  (let ((__function__ 'all-addresses-valid?))
    (declare (ignorable __function__))
    (if (endp addresses)
        t
      (and (address-valid-p (first addresses))
           (all-addresses-valid? (rest addresses))))))

Theorem: booleanp-of-all-addresses-valid?

(defthm booleanp-of-all-addresses-valid?
  (b* ((y/n (all-addresses-valid? addresses)))
    (booleanp y/n))
  :rule-classes :rewrite)