Abstract a
(abs-*-definition trees) → definitions
Function:
(defun abs-*-definition (trees) (declare (xargs :guard (abnf::tree-listp trees))) (let ((__function__ 'abs-*-definition)) (declare (ignorable __function__)) (b* (((when (endp trees)) nil) ((okf definition) (abs-definition (car trees))) ((okf definitions) (abs-*-definition (cdr trees)))) (cons definition definitions))))
Theorem:
(defthm definition-list-resultp-of-abs-*-definition (b* ((definitions (abs-*-definition trees))) (definition-list-resultp definitions)) :rule-classes :rewrite)
Theorem:
(defthm definition-listp-of-abs-*-definition (b* ((?definitions (abs-*-definition trees))) (implies (not (reserrp definitions)) (definition-listp definitions))))
Theorem:
(defthm abs-*-definition-of-tree-list-fix-trees (equal (abs-*-definition (abnf::tree-list-fix trees)) (abs-*-definition trees)))
Theorem:
(defthm abs-*-definition-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv trees trees-equiv) (equal (abs-*-definition trees) (abs-*-definition trees-equiv))) :rule-classes :congruence)