A list of zero or more
(abstract-*-dot-1*hexdig trees) → nats
Function:
(defun abstract-*-dot-1*hexdig (trees) (declare (xargs :guard (tree-listp trees))) (b* (((when (endp trees)) nil) (nat (abstract-dot/dash-1*hexdig (car trees))) (nats (abstract-*-dot-1*hexdig (cdr trees)))) (cons nat nats)))
Theorem:
(defthm nat-listp-of-abstract-*-dot-1*hexdig (b* ((nats (abstract-*-dot-1*hexdig trees))) (nat-listp nats)) :rule-classes :rewrite)