Check if an ABNF tree is a non-leaf tree with a given optional rule name or no rule name as root and a list of one list of one subtree, where the subtree is a leaf tree whose natural numbers match a given sequence of natural numbers.
(check-tree-nonleaf-num-seq tree rulename? nats) → pass
Function:
(defun check-tree-nonleaf-num-seq (tree rulename? nats) (declare (xargs :guard (and (abnf::treep tree) (maybe-stringp rulename?) (nat-listp nats)))) (let ((__function__ 'check-tree-nonleaf-num-seq)) (declare (ignorable __function__)) (b* (((okf tree) (check-tree-nonleaf-1-1 tree rulename?))) (check-tree-num-seq tree nats))))
Theorem:
(defthm pass-resultp-of-check-tree-nonleaf-num-seq (b* ((pass (check-tree-nonleaf-num-seq tree rulename? nats))) (pass-resultp pass)) :rule-classes :rewrite)
Theorem:
(defthm check-tree-nonleaf-num-seq-of-tree-fix-tree (equal (check-tree-nonleaf-num-seq (abnf::tree-fix tree) rulename? nats) (check-tree-nonleaf-num-seq tree rulename? nats)))
Theorem:
(defthm check-tree-nonleaf-num-seq-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (check-tree-nonleaf-num-seq tree rulename? nats) (check-tree-nonleaf-num-seq tree-equiv rulename? nats))) :rule-classes :congruence)
Theorem:
(defthm check-tree-nonleaf-num-seq-of-maybe-string-fix-rulename? (equal (check-tree-nonleaf-num-seq tree (maybe-string-fix rulename?) nats) (check-tree-nonleaf-num-seq tree rulename? nats)))
Theorem:
(defthm check-tree-nonleaf-num-seq-maybe-string-equiv-congruence-on-rulename? (implies (acl2::maybe-string-equiv rulename? rulename?-equiv) (equal (check-tree-nonleaf-num-seq tree rulename? nats) (check-tree-nonleaf-num-seq tree rulename?-equiv nats))) :rule-classes :congruence)
Theorem:
(defthm check-tree-nonleaf-num-seq-of-nat-list-fix-nats (equal (check-tree-nonleaf-num-seq tree rulename? (nat-list-fix nats)) (check-tree-nonleaf-num-seq tree rulename? nats)))
Theorem:
(defthm check-tree-nonleaf-num-seq-nat-list-equiv-congruence-on-nats (implies (acl2::nat-list-equiv nats nats-equiv) (equal (check-tree-nonleaf-num-seq tree rulename? nats) (check-tree-nonleaf-num-seq tree rulename? nats-equiv))) :rule-classes :congruence)