Abstract a
(abs-?-identifier-*-comma-identifier tree) → ids
Function:
(defun abs-?-identifier-*-comma-identifier (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-?-identifier-*-comma-identifier)) (declare (ignorable __function__)) (b* (((okf treess) (check-tree-nonleaf tree nil)) ((when (endp treess)) nil) ((okf (abnf::tree-list-tuple2 sub)) (check-tree-list-list-2 treess)) ((okf tree) (check-tree-list-1 sub.1st)) ((okf id) (abs-identifier tree)) ((okf ids) (abs-*-comma-identifier sub.2nd))) (cons id ids))))
Theorem:
(defthm string-list-resultp-of-abs-?-identifier-*-comma-identifier (b* ((ids (abs-?-identifier-*-comma-identifier tree))) (string-list-resultp ids)) :rule-classes :rewrite)
Theorem:
(defthm identifier-listp-of-abs-?-identifier-*-comma-identifier (b* ((?ids (abs-?-identifier-*-comma-identifier tree))) (implies (not (reserrp ids)) (string-listp ids))))
Theorem:
(defthm abs-?-identifier-*-comma-identifier-of-tree-fix-tree (equal (abs-?-identifier-*-comma-identifier (abnf::tree-fix tree)) (abs-?-identifier-*-comma-identifier tree)))
Theorem:
(defthm abs-?-identifier-*-comma-identifier-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-?-identifier-*-comma-identifier tree) (abs-?-identifier-*-comma-identifier tree-equiv))) :rule-classes :congruence)