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