		Search-engine friendly clone of the ACL2 documentation.

Reasoning-about-memory-reads-and-writes

Canonical-address-listp

Recognizer of a list of canonical addresses

Signature
(canonical-address-listp lst) → *

Definitions and Theorems

Function: canonical-address-listp

(defun canonical-address-listp (lst)
  (declare (xargs :guard t))
  (let ((__function__ 'canonical-address-listp))
    (declare (ignorable __function__))
    (if (equal lst nil)
        t
      (and (consp lst)
           (canonical-address-p (car lst))
           (canonical-address-listp (cdr lst))))))

Theorem: cdr-canonical-address-listp

(defthm cdr-canonical-address-listp
  (implies (canonical-address-listp x)
           (canonical-address-listp (cdr x))))