Check if an ABNF tree is a leaf tree whose natural numbers match a given sequence of natural numbers.
(check-tree-num-seq tree nats) → pass
Function:
(defun check-tree-num-seq (tree nats) (declare (xargs :guard (and (abnf::treep tree) (nat-listp nats)))) (let ((__function__ 'check-tree-num-seq)) (declare (ignorable __function__)) (b* ((nats (nat-list-fix nats)) ((okf tree-nats) (check-tree-leafterm tree))) (if (equal tree-nats nats) :pass (reserrf (list :required (list :seq nats) :found (tree-info-for-error tree)))))))
Theorem:
(defthm pass-resultp-of-check-tree-num-seq (b* ((pass (check-tree-num-seq tree nats))) (pass-resultp pass)) :rule-classes :rewrite)
Theorem:
(defthm check-tree-num-seq-of-tree-fix-tree (equal (check-tree-num-seq (abnf::tree-fix tree) nats) (check-tree-num-seq tree nats)))
Theorem:
(defthm check-tree-num-seq-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (check-tree-num-seq tree nats) (check-tree-num-seq tree-equiv nats))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-seq-of-nat-list-fix-nats (equal (check-tree-num-seq tree (nat-list-fix nats)) (check-tree-num-seq tree nats)))
Theorem:
(defthm check-tree-num-seq-nat-list-equiv-congruence-on-nats (implies (acl2::nat-list-equiv nats nats-equiv) (equal (check-tree-num-seq tree nats) (check-tree-num-seq tree nats-equiv))) :rule-classes :congruence)