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