		Search-engine friendly clone of the ACL2 documentation.

Abnf-tree-utilities

Check-tree-nonleaf-4

Check if an ABNF tree has a given rule name or no rule name as root and a list of four lists of subtrees, returning those lists of subtrees if successful.

Signature
(check-tree-nonleaf-4 tree rulename?) → sub
Arguments: tree — Guard (abnf::treep tree).; rulename? — Guard (maybe-stringp rulename?).
Returns: sub — Type (abnf::tree-list-tuple4-resultp sub).

Definitions and Theorems

Function: check-tree-nonleaf-4

(defun check-tree-nonleaf-4 (tree rulename?)
  (declare (xargs :guard (and (abnf::treep tree)
                              (maybe-stringp rulename?))))
  (let ((__function__ 'check-tree-nonleaf-4))
    (declare (ignorable __function__))
    (b* (((okf treess)
          (check-tree-nonleaf tree rulename?)))
      (check-tree-list-list-4 treess))))

Theorem: tree-list-tuple4-resultp-of-check-tree-nonleaf-4

(defthm tree-list-tuple4-resultp-of-check-tree-nonleaf-4
  (b* ((sub (check-tree-nonleaf-4 tree rulename?)))
    (abnf::tree-list-tuple4-resultp sub))
  :rule-classes :rewrite)

Theorem: tree-count-of-check-tree-nonleaf-4

(defthm tree-count-of-check-tree-nonleaf-4
 (b* ((?sub (check-tree-nonleaf-4 tree rulename?)))
  (implies
   (not (reserrp sub))
   (and (< (abnf::tree-list-count (abnf::tree-list-tuple4->1st sub))
           (abnf::tree-count tree))
        (< (abnf::tree-list-count (abnf::tree-list-tuple4->2nd sub))
           (abnf::tree-count tree))
        (< (abnf::tree-list-count (abnf::tree-list-tuple4->3rd sub))
           (abnf::tree-count tree))
        (< (abnf::tree-list-count (abnf::tree-list-tuple4->4th sub))
           (abnf::tree-count tree)))))
 :rule-classes :linear)

Theorem: check-tree-nonleaf-4-of-tree-fix-tree

(defthm check-tree-nonleaf-4-of-tree-fix-tree
  (equal (check-tree-nonleaf-4 (abnf::tree-fix tree)
                               rulename?)
         (check-tree-nonleaf-4 tree rulename?)))

Theorem: check-tree-nonleaf-4-tree-equiv-congruence-on-tree

(defthm check-tree-nonleaf-4-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (check-tree-nonleaf-4 tree rulename?)
                  (check-tree-nonleaf-4 tree-equiv rulename?)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-4-of-maybe-string-fix-rulename?

(defthm check-tree-nonleaf-4-of-maybe-string-fix-rulename?
  (equal (check-tree-nonleaf-4 tree (maybe-string-fix rulename?))
         (check-tree-nonleaf-4 tree rulename?)))

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

(defthm
    check-tree-nonleaf-4-maybe-string-equiv-congruence-on-rulename?
  (implies (acl2::maybe-string-equiv rulename? rulename?-equiv)
           (equal (check-tree-nonleaf-4 tree rulename?)
                  (check-tree-nonleaf-4 tree rulename?-equiv)))
  :rule-classes :congruence)