A list of zero or more
(abstract-*-alpha/digit/dash trees) → chars
Function:
(defun abstract-*-alpha/digit/dash (trees) (declare (xargs :guard (tree-listp trees))) (b* (((when (endp trees)) nil) ((cons tree trees) trees) (char (abstract-alpha/digit/dash tree)) (chars (abstract-*-alpha/digit/dash trees))) (cons char chars)))
Theorem:
(defthm character-listp-of-abstract-*-alpha/digit/dash (b* ((chars (abstract-*-alpha/digit/dash trees))) (character-listp chars)) :rule-classes :rewrite)