		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-nonleaf-1-1

Check if an ABNF tree has a given rule name or no rule name as root and a list of one list of one subtree, returning the subtree if successful.

Signature
(check-tree-nonleaf-1-1 tree rulename?) → sub
Arguments: tree — Guard (treep tree).; rulename? — Guard (acl2::maybe-stringp rulename?).
Returns: sub — Type (tree-resultp sub).

Definitions and Theorems

Function: check-tree-nonleaf-1-1

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

Theorem: tree-resultp-of-check-tree-nonleaf-1-1

(defthm tree-resultp-of-check-tree-nonleaf-1-1
  (b* ((sub (check-tree-nonleaf-1-1 tree rulename?)))
    (tree-resultp sub))
  :rule-classes :rewrite)

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

(defthm tree-count-of-check-tree-nonleaf-1-1
  (b* ((?sub (check-tree-nonleaf-1-1 tree rulename?)))
    (implies (not (reserrp sub))
             (< (tree-count sub) (tree-count tree))))
  :rule-classes :linear)

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

(defthm check-tree-nonleaf-1-1-of-tree-fix-tree
  (equal (check-tree-nonleaf-1-1 (tree-fix tree)
                                 rulename?)
         (check-tree-nonleaf-1-1 tree rulename?)))

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

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

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

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

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

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