Recognizer of a list of canonical addresses
(canonical-address-listp lst) → *
Function:
(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:
(defthm cdr-canonical-address-listp (implies (canonical-address-listp x) (canonical-address-listp (cdr x))))