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