Abstract a
(abs-?-expression-*-comma-expression tree) → exprs
Function:
(defun abs-?-expression-*-comma-expression (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-?-expression-*-comma-expression)) (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 expr) (abs-expression tree)) ((okf exprs) (abs-*-comma-expression sub.2nd))) (cons expr exprs))))
Theorem:
(defthm expression-list-resultp-of-abs-?-expression-*-comma-expression (b* ((exprs (abs-?-expression-*-comma-expression tree))) (expression-list-resultp exprs)) :rule-classes :rewrite)
Theorem:
(defthm expression-listp-of-abs-?-expression-*-comma-expression (b* ((?exprs (abs-?-expression-*-comma-expression tree))) (implies (not (reserrp exprs)) (expression-listp exprs))))
Theorem:
(defthm abs-?-expression-*-comma-expression-of-tree-fix-tree (equal (abs-?-expression-*-comma-expression (abnf::tree-fix tree)) (abs-?-expression-*-comma-expression tree)))
Theorem:
(defthm abs-?-expression-*-comma-expression-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-?-expression-*-comma-expression tree) (abs-?-expression-*-comma-expression tree-equiv))) :rule-classes :congruence)