		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-num-seq

Check if an ABNF tree is a leaf tree whose natural numbers match a given sequence of natural numbers.

Signature
(check-tree-num-seq tree nats) → pass
Arguments: tree — Guard (treep tree).; nats — Guard (nat-listp nats).
Returns: pass — Type (pass-resultp pass).

Definitions and Theorems

Function: check-tree-num-seq

(defun check-tree-num-seq (tree nats)
  (declare (xargs :guard (and (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: pass-resultp-of-check-tree-num-seq

(defthm pass-resultp-of-check-tree-num-seq
  (b* ((pass (check-tree-num-seq tree nats)))
    (pass-resultp pass))
  :rule-classes :rewrite)

Theorem: check-tree-num-seq-of-tree-fix-tree

(defthm check-tree-num-seq-of-tree-fix-tree
  (equal (check-tree-num-seq (tree-fix tree)
                             nats)
         (check-tree-num-seq tree nats)))

Theorem: check-tree-num-seq-tree-equiv-congruence-on-tree

(defthm check-tree-num-seq-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (check-tree-num-seq tree nats)
                  (check-tree-num-seq tree-equiv nats)))
  :rule-classes :congruence)

Theorem: check-tree-num-seq-of-nat-list-fix-nats

(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: check-tree-num-seq-nat-list-equiv-congruence-on-nats

(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)