		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-nonleaf-num-seq

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.

Signature
(check-tree-nonleaf-num-seq tree rulename? nats) → pass
Arguments: tree — Guard (treep tree).; rulename? — Guard (acl2::maybe-stringp rulename?).; nats — Guard (nat-listp nats).
Returns: pass — Type (pass-resultp pass).

Definitions and Theorems

Function: check-tree-nonleaf-num-seq

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

(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: check-tree-nonleaf-num-seq-of-tree-fix-tree

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

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

(defthm check-tree-nonleaf-num-seq-tree-equiv-congruence-on-tree
 (implies
     (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: check-tree-nonleaf-num-seq-of-maybe-string-fix-rulename?

(defthm check-tree-nonleaf-num-seq-of-maybe-string-fix-rulename?
  (equal (check-tree-nonleaf-num-seq
              tree (acl2::maybe-string-fix rulename?)
              nats)
         (check-tree-nonleaf-num-seq tree rulename? nats)))

Theorem: check-tree-nonleaf-num-seq-maybe-string-equiv-congruence-on-rulename?

(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: check-tree-nonleaf-num-seq-of-nat-list-fix-nats

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

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