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