Check if a tree is
(check-?-comma tree) → pass
Function:
(defun check-?-comma (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'check-?-comma)) (declare (ignorable __function__)) (b* (((okf treess) (check-tree-nonleaf tree nil)) ((when (endp treess)) :pass) ((okf trees) (check-tree-list-list-1 treess)) ((okf tree) (check-tree-list-1 trees))) (check-tree-ichars tree ","))))
Theorem:
(defthm pass-resultp-of-check-?-comma (b* ((pass (check-?-comma tree))) (pass-resultp pass)) :rule-classes :rewrite)
Theorem:
(defthm check-?-comma-of-tree-fix-tree (equal (check-?-comma (abnf::tree-fix tree)) (check-?-comma tree)))
Theorem:
(defthm check-?-comma-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (check-?-comma tree) (check-?-comma tree-equiv))) :rule-classes :congruence)