Abstract a
(abs-*-letter/decimaldigit/underscore trees) → chars
Function:
(defun abs-*-letter/decimaldigit/underscore (trees) (declare (xargs :guard (abnf::tree-listp trees))) (let ((__function__ 'abs-*-letter/decimaldigit/underscore)) (declare (ignorable __function__)) (b* (((when (endp trees)) nil) ((okf char) (abs-letter/decimaldigit/underscore (car trees))) ((okf chars) (abs-*-letter/decimaldigit/underscore (cdr trees)))) (cons char chars))))
Theorem:
(defthm character-list-resultp-of-abs-*-letter/decimaldigit/underscore (b* ((chars (abs-*-letter/decimaldigit/underscore trees))) (character-list-resultp chars)) :rule-classes :rewrite)
Theorem:
(defthm letter/digit/uscore-char-listp-of-abs-*-letter/decimaldigit/underscore (b* ((?chars (abs-*-letter/decimaldigit/underscore trees))) (implies (not (reserrp chars)) (str::letter/digit/uscore-charlist-p chars))))
Theorem:
(defthm abs-*-letter/decimaldigit/underscore-of-tree-list-fix-trees (equal (abs-*-letter/decimaldigit/underscore (abnf::tree-list-fix trees)) (abs-*-letter/decimaldigit/underscore trees)))
Theorem:
(defthm abs-*-letter/decimaldigit/underscore-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv trees trees-equiv) (equal (abs-*-letter/decimaldigit/underscore trees) (abs-*-letter/decimaldigit/underscore trees-equiv))) :rule-classes :congruence)