		Search-engine friendly clone of the ACL2 documentation.

*grammar-old*

grammar-old-tree-operations

Tree operations specialized to *grammar-old*.

Definitions and Theorems

Function: ocst-matchp$

(defun ocst-matchp$ (abnf::tree abnf::elem)
  (declare (xargs :guard (and (abnf::treep abnf::tree)
                              (abnf::elementp abnf::elem))))
  (let ((__function__ 'ocst-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-terminatedp abnf::tree)
         (abnf::tree-match-element-p
              abnf::tree abnf::elem *grammar-old*))))

Theorem: booleanp-of-ocst-matchp$

(defthm booleanp-of-ocst-matchp$
  (b* ((abnf::yes/no (ocst-matchp$ abnf::tree abnf::elem)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: ocst-matchp$-of-tree-fix-tree

(defthm ocst-matchp$-of-tree-fix-tree
  (equal (ocst-matchp$ (abnf::tree-fix abnf::tree)
                       abnf::elem)
         (ocst-matchp$ abnf::tree abnf::elem)))

Theorem: ocst-matchp$-tree-equiv-congruence-on-tree

(defthm ocst-matchp$-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv abnf::tree tree-equiv)
           (equal (ocst-matchp$ abnf::tree abnf::elem)
                  (ocst-matchp$ tree-equiv abnf::elem)))
  :rule-classes :congruence)

Theorem: ocst-matchp$-of-element-fix-elem

(defthm ocst-matchp$-of-element-fix-elem
  (equal (ocst-matchp$ abnf::tree
                       (abnf::element-fix abnf::elem))
         (ocst-matchp$ abnf::tree abnf::elem)))

Theorem: ocst-matchp$-element-equiv-congruence-on-elem

(defthm ocst-matchp$-element-equiv-congruence-on-elem
  (implies (abnf::element-equiv abnf::elem elem-equiv)
           (equal (ocst-matchp$ abnf::tree abnf::elem)
                  (ocst-matchp$ abnf::tree elem-equiv)))
  :rule-classes :congruence)

Function: ocst-list-elem-matchp$

(defun ocst-list-elem-matchp$ (abnf::trees abnf::elem)
  (declare (xargs :guard (and (abnf::tree-listp abnf::trees)
                              (abnf::elementp abnf::elem))))
  (let ((__function__ 'ocst-list-elem-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-terminatedp abnf::trees)
         (abnf::tree-list-match-element-p
              abnf::trees abnf::elem *grammar-old*))))

Theorem: booleanp-of-ocst-list-elem-matchp$

(defthm booleanp-of-ocst-list-elem-matchp$
  (b*
    ((abnf::yes/no (ocst-list-elem-matchp$ abnf::trees abnf::elem)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: ocst-list-elem-matchp$-of-tree-list-fix-trees

(defthm ocst-list-elem-matchp$-of-tree-list-fix-trees
  (equal (ocst-list-elem-matchp$ (abnf::tree-list-fix abnf::trees)
                                 abnf::elem)
         (ocst-list-elem-matchp$ abnf::trees abnf::elem)))

Theorem: ocst-list-elem-matchp$-tree-list-equiv-congruence-on-trees

(defthm ocst-list-elem-matchp$-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv abnf::trees trees-equiv)
           (equal (ocst-list-elem-matchp$ abnf::trees abnf::elem)
                  (ocst-list-elem-matchp$ trees-equiv abnf::elem)))
  :rule-classes :congruence)

Theorem: ocst-list-elem-matchp$-of-element-fix-elem

(defthm ocst-list-elem-matchp$-of-element-fix-elem
  (equal (ocst-list-elem-matchp$ abnf::trees
                                 (abnf::element-fix abnf::elem))
         (ocst-list-elem-matchp$ abnf::trees abnf::elem)))

Theorem: ocst-list-elem-matchp$-element-equiv-congruence-on-elem

(defthm ocst-list-elem-matchp$-element-equiv-congruence-on-elem
  (implies (abnf::element-equiv abnf::elem elem-equiv)
           (equal (ocst-list-elem-matchp$ abnf::trees abnf::elem)
                  (ocst-list-elem-matchp$ abnf::trees elem-equiv)))
  :rule-classes :congruence)

Function: ocst-list-rep-matchp$

(defun ocst-list-rep-matchp$ (abnf::trees abnf::rep)
  (declare (xargs :guard (and (abnf::tree-listp abnf::trees)
                              (abnf::repetitionp abnf::rep))))
  (let ((__function__ 'ocst-list-rep-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-terminatedp abnf::trees)
         (abnf::tree-list-match-repetition-p
              abnf::trees abnf::rep *grammar-old*))))

Theorem: booleanp-of-ocst-list-rep-matchp$

(defthm booleanp-of-ocst-list-rep-matchp$
  (b* ((abnf::yes/no (ocst-list-rep-matchp$ abnf::trees abnf::rep)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: ocst-list-rep-matchp$-of-tree-list-fix-trees

(defthm ocst-list-rep-matchp$-of-tree-list-fix-trees
  (equal (ocst-list-rep-matchp$ (abnf::tree-list-fix abnf::trees)
                                abnf::rep)
         (ocst-list-rep-matchp$ abnf::trees abnf::rep)))

Theorem: ocst-list-rep-matchp$-tree-list-equiv-congruence-on-trees

(defthm ocst-list-rep-matchp$-tree-list-equiv-congruence-on-trees
  (implies (abnf::tree-list-equiv abnf::trees trees-equiv)
           (equal (ocst-list-rep-matchp$ abnf::trees abnf::rep)
                  (ocst-list-rep-matchp$ trees-equiv abnf::rep)))
  :rule-classes :congruence)

Theorem: ocst-list-rep-matchp$-of-repetition-fix-rep

(defthm ocst-list-rep-matchp$-of-repetition-fix-rep
  (equal (ocst-list-rep-matchp$ abnf::trees
                                (abnf::repetition-fix abnf::rep))
         (ocst-list-rep-matchp$ abnf::trees abnf::rep)))

Theorem: ocst-list-rep-matchp$-repetition-equiv-congruence-on-rep

(defthm ocst-list-rep-matchp$-repetition-equiv-congruence-on-rep
  (implies (abnf::repetition-equiv abnf::rep rep-equiv)
           (equal (ocst-list-rep-matchp$ abnf::trees abnf::rep)
                  (ocst-list-rep-matchp$ abnf::trees rep-equiv)))
  :rule-classes :congruence)

Function: ocst-list-list-conc-matchp$

(defun ocst-list-list-conc-matchp$ (abnf::treess abnf::conc)
  (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess)
                              (abnf::concatenationp abnf::conc))))
  (let ((__function__ 'ocst-list-list-conc-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-list-terminatedp abnf::treess)
         (abnf::tree-list-list-match-concatenation-p
              abnf::treess
              abnf::conc *grammar-old*))))

Theorem: booleanp-of-ocst-list-list-conc-matchp$

(defthm booleanp-of-ocst-list-list-conc-matchp$
  (b* ((abnf::yes/no
            (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: ocst-list-list-conc-matchp$-of-tree-list-list-fix-treess

(defthm ocst-list-list-conc-matchp$-of-tree-list-list-fix-treess
  (equal (ocst-list-list-conc-matchp$
              (abnf::tree-list-list-fix abnf::treess)
              abnf::conc)
         (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)))

Theorem: ocst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess

(defthm
 ocst-list-list-conc-matchp$-tree-list-list-equiv-congruence-on-treess
 (implies
      (abnf::tree-list-list-equiv abnf::treess treess-equiv)
      (equal (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)
             (ocst-list-list-conc-matchp$ treess-equiv abnf::conc)))
 :rule-classes :congruence)

Theorem: ocst-list-list-conc-matchp$-of-concatenation-fix-conc

(defthm ocst-list-list-conc-matchp$-of-concatenation-fix-conc
 (equal
  (ocst-list-list-conc-matchp$ abnf::treess
                               (abnf::concatenation-fix abnf::conc))
  (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)))

Theorem: ocst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc

(defthm
 ocst-list-list-conc-matchp$-concatenation-equiv-congruence-on-conc
 (implies
      (abnf::concatenation-equiv abnf::conc conc-equiv)
      (equal (ocst-list-list-conc-matchp$ abnf::treess abnf::conc)
             (ocst-list-list-conc-matchp$ abnf::treess conc-equiv)))
 :rule-classes :congruence)

Function: ocst-list-list-alt-matchp$

(defun ocst-list-list-alt-matchp$ (abnf::treess abnf::alt)
  (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess)
                              (abnf::alternationp abnf::alt))))
  (let ((__function__ 'ocst-list-list-alt-matchp$))
    (declare (ignorable __function__))
    (and (abnf::tree-list-list-terminatedp abnf::treess)
         (abnf::tree-list-list-match-alternation-p
              abnf::treess abnf::alt *grammar-old*))))

Theorem: booleanp-of-ocst-list-list-alt-matchp$

(defthm booleanp-of-ocst-list-list-alt-matchp$
  (b* ((abnf::yes/no
            (ocst-list-list-alt-matchp$ abnf::treess abnf::alt)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: ocst-list-list-alt-matchp$-of-tree-list-list-fix-treess

(defthm ocst-list-list-alt-matchp$-of-tree-list-list-fix-treess
  (equal (ocst-list-list-alt-matchp$
              (abnf::tree-list-list-fix abnf::treess)
              abnf::alt)
         (ocst-list-list-alt-matchp$ abnf::treess abnf::alt)))

Theorem: ocst-list-list-alt-matchp$-tree-list-list-equiv-congruence-on-treess

(defthm
 ocst-list-list-alt-matchp$-tree-list-list-equiv-congruence-on-treess
 (implies
      (abnf::tree-list-list-equiv abnf::treess treess-equiv)
      (equal (ocst-list-list-alt-matchp$ abnf::treess abnf::alt)
             (ocst-list-list-alt-matchp$ treess-equiv abnf::alt)))
 :rule-classes :congruence)

Theorem: ocst-list-list-alt-matchp$-of-alternation-fix-alt

(defthm ocst-list-list-alt-matchp$-of-alternation-fix-alt
 (equal
      (ocst-list-list-alt-matchp$ abnf::treess
                                  (abnf::alternation-fix abnf::alt))
      (ocst-list-list-alt-matchp$ abnf::treess abnf::alt)))

Theorem: ocst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt

(defthm
     ocst-list-list-alt-matchp$-alternation-equiv-congruence-on-alt
  (implies
       (abnf::alternation-equiv abnf::alt alt-equiv)
       (equal (ocst-list-list-alt-matchp$ abnf::treess abnf::alt)
              (ocst-list-list-alt-matchp$ abnf::treess alt-equiv)))
  :rule-classes :congruence)

Function: ocst-%x0-9-nat

(defun ocst-%x0-9-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x0-9")))
  (let ((__function__ 'ocst-%x0-9-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x0-9-nat

(defthm natp-of-ocst-%x0-9-nat
  (b* ((nat (ocst-%x0-9-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x0-9-nat-of-tree-fix-cst

(defthm ocst-%x0-9-nat-of-tree-fix-cst
  (equal (ocst-%x0-9-nat (abnf::tree-fix abnf::cst))
         (ocst-%x0-9-nat abnf::cst)))

Theorem: ocst-%x0-9-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x0-9-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x0-9-nat abnf::cst)
                  (ocst-%x0-9-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%x0-10ffff-nat

(defun ocst-%x0-10ffff-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x0-10FFFF")))
  (let ((__function__ 'ocst-%x0-10ffff-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x0-10ffff-nat

(defthm natp-of-ocst-%x0-10ffff-nat
  (b* ((nat (ocst-%x0-10ffff-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x0-10ffff-nat-of-tree-fix-cst

(defthm ocst-%x0-10ffff-nat-of-tree-fix-cst
  (equal (ocst-%x0-10ffff-nat (abnf::tree-fix abnf::cst))
         (ocst-%x0-10ffff-nat abnf::cst)))

Theorem: ocst-%x0-10ffff-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x0-10ffff-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x0-10ffff-nat abnf::cst)
                  (ocst-%x0-10ffff-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%xb-c-nat

(defun ocst-%xb-c-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%xB-C")))
  (let ((__function__ 'ocst-%xb-c-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%xb-c-nat

(defthm natp-of-ocst-%xb-c-nat
  (b* ((nat (ocst-%xb-c-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%xb-c-nat-of-tree-fix-cst

(defthm ocst-%xb-c-nat-of-tree-fix-cst
  (equal (ocst-%xb-c-nat (abnf::tree-fix abnf::cst))
         (ocst-%xb-c-nat abnf::cst)))

Theorem: ocst-%xb-c-nat-tree-equiv-congruence-on-cst

(defthm ocst-%xb-c-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%xb-c-nat abnf::cst)
                  (ocst-%xb-c-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%xe-21-nat

(defun ocst-%xe-21-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%xE-21")))
  (let ((__function__ 'ocst-%xe-21-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%xe-21-nat

(defthm natp-of-ocst-%xe-21-nat
  (b* ((nat (ocst-%xe-21-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%xe-21-nat-of-tree-fix-cst

(defthm ocst-%xe-21-nat-of-tree-fix-cst
  (equal (ocst-%xe-21-nat (abnf::tree-fix abnf::cst))
         (ocst-%xe-21-nat abnf::cst)))

Theorem: ocst-%xe-21-nat-tree-equiv-congruence-on-cst

(defthm ocst-%xe-21-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%xe-21-nat abnf::cst)
                  (ocst-%xe-21-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%x23-5b-nat

(defun ocst-%x23-5b-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x23-5B")))
  (let ((__function__ 'ocst-%x23-5b-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x23-5b-nat

(defthm natp-of-ocst-%x23-5b-nat
  (b* ((nat (ocst-%x23-5b-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x23-5b-nat-of-tree-fix-cst

(defthm ocst-%x23-5b-nat-of-tree-fix-cst
  (equal (ocst-%x23-5b-nat (abnf::tree-fix abnf::cst))
         (ocst-%x23-5b-nat abnf::cst)))

Theorem: ocst-%x23-5b-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x23-5b-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x23-5b-nat abnf::cst)
                  (ocst-%x23-5b-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%x30-39-nat

(defun ocst-%x30-39-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x30-39")))
  (let ((__function__ 'ocst-%x30-39-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x30-39-nat

(defthm natp-of-ocst-%x30-39-nat
  (b* ((nat (ocst-%x30-39-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x30-39-nat-of-tree-fix-cst

(defthm ocst-%x30-39-nat-of-tree-fix-cst
  (equal (ocst-%x30-39-nat (abnf::tree-fix abnf::cst))
         (ocst-%x30-39-nat abnf::cst)))

Theorem: ocst-%x30-39-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x30-39-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x30-39-nat abnf::cst)
                  (ocst-%x30-39-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%x41-5a-nat

(defun ocst-%x41-5a-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x41-5A")))
  (let ((__function__ 'ocst-%x41-5a-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x41-5a-nat

(defthm natp-of-ocst-%x41-5a-nat
  (b* ((nat (ocst-%x41-5a-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x41-5a-nat-of-tree-fix-cst

(defthm ocst-%x41-5a-nat-of-tree-fix-cst
  (equal (ocst-%x41-5a-nat (abnf::tree-fix abnf::cst))
         (ocst-%x41-5a-nat abnf::cst)))

Theorem: ocst-%x41-5a-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x41-5a-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x41-5a-nat abnf::cst)
                  (ocst-%x41-5a-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%x5d-10ffff-nat

(defun ocst-%x5d-10ffff-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x5D-10FFFF")))
  (let ((__function__ 'ocst-%x5d-10ffff-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x5d-10ffff-nat

(defthm natp-of-ocst-%x5d-10ffff-nat
  (b* ((nat (ocst-%x5d-10ffff-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x5d-10ffff-nat-of-tree-fix-cst

(defthm ocst-%x5d-10ffff-nat-of-tree-fix-cst
  (equal (ocst-%x5d-10ffff-nat (abnf::tree-fix abnf::cst))
         (ocst-%x5d-10ffff-nat abnf::cst)))

Theorem: ocst-%x5d-10ffff-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x5d-10ffff-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x5d-10ffff-nat abnf::cst)
                  (ocst-%x5d-10ffff-nat cst-equiv)))
  :rule-classes :congruence)

Function: ocst-%x61-7a-nat

(defun ocst-%x61-7a-nat (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "%x61-7A")))
  (let ((__function__ 'ocst-%x61-7a-nat))
    (declare (ignorable __function__))
    (acl2::lnfix (nth 0
                      (abnf::tree-leafterm->get abnf::cst)))))

Theorem: natp-of-ocst-%x61-7a-nat

(defthm natp-of-ocst-%x61-7a-nat
  (b* ((nat (ocst-%x61-7a-nat abnf::cst)))
    (natp nat))
  :rule-classes :rewrite)

Theorem: ocst-%x61-7a-nat-of-tree-fix-cst

(defthm ocst-%x61-7a-nat-of-tree-fix-cst
  (equal (ocst-%x61-7a-nat (abnf::tree-fix abnf::cst))
         (ocst-%x61-7a-nat abnf::cst)))

Theorem: ocst-%x61-7a-nat-tree-equiv-congruence-on-cst

(defthm ocst-%x61-7a-nat-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-%x61-7a-nat abnf::cst)
                  (ocst-%x61-7a-nat cst-equiv)))
  :rule-classes :congruence)

Theorem: ocst-%x0-9-nat-bounds

(defthm ocst-%x0-9-nat-bounds
  (implies (ocst-matchp abnf::cst "%x0-9")
           (and (<= 0 (ocst-%x0-9-nat abnf::cst))
                (<= (ocst-%x0-9-nat abnf::cst) 9)))
  :rule-classes :linear)

Theorem: ocst-%x0-10ffff-nat-bounds

(defthm ocst-%x0-10ffff-nat-bounds
  (implies (ocst-matchp abnf::cst "%x0-10FFFF")
           (and (<= 0 (ocst-%x0-10ffff-nat abnf::cst))
                (<= (ocst-%x0-10ffff-nat abnf::cst)
                    1114111)))
  :rule-classes :linear)

Theorem: ocst-%xb-c-nat-bounds

(defthm ocst-%xb-c-nat-bounds
  (implies (ocst-matchp abnf::cst "%xB-C")
           (and (<= 11 (ocst-%xb-c-nat abnf::cst))
                (<= (ocst-%xb-c-nat abnf::cst) 12)))
  :rule-classes :linear)

Theorem: ocst-%xe-21-nat-bounds

(defthm ocst-%xe-21-nat-bounds
  (implies (ocst-matchp abnf::cst "%xE-21")
           (and (<= 14 (ocst-%xe-21-nat abnf::cst))
                (<= (ocst-%xe-21-nat abnf::cst) 33)))
  :rule-classes :linear)

Theorem: ocst-%x23-5b-nat-bounds

(defthm ocst-%x23-5b-nat-bounds
  (implies (ocst-matchp abnf::cst "%x23-5B")
           (and (<= 35 (ocst-%x23-5b-nat abnf::cst))
                (<= (ocst-%x23-5b-nat abnf::cst) 91)))
  :rule-classes :linear)

Theorem: ocst-%x30-39-nat-bounds

(defthm ocst-%x30-39-nat-bounds
  (implies (ocst-matchp abnf::cst "%x30-39")
           (and (<= 48 (ocst-%x30-39-nat abnf::cst))
                (<= (ocst-%x30-39-nat abnf::cst) 57)))
  :rule-classes :linear)

Theorem: ocst-%x41-5a-nat-bounds

(defthm ocst-%x41-5a-nat-bounds
  (implies (ocst-matchp abnf::cst "%x41-5A")
           (and (<= 65 (ocst-%x41-5a-nat abnf::cst))
                (<= (ocst-%x41-5a-nat abnf::cst) 90)))
  :rule-classes :linear)

Theorem: ocst-%x5d-10ffff-nat-bounds

(defthm ocst-%x5d-10ffff-nat-bounds
  (implies (ocst-matchp abnf::cst "%x5D-10FFFF")
           (and (<= 93 (ocst-%x5d-10ffff-nat abnf::cst))
                (<= (ocst-%x5d-10ffff-nat abnf::cst)
                    1114111)))
  :rule-classes :linear)

Theorem: ocst-%x61-7a-nat-bounds

(defthm ocst-%x61-7a-nat-bounds
  (implies (ocst-matchp abnf::cst "%x61-7A")
           (and (<= 97 (ocst-%x61-7a-nat abnf::cst))
                (<= (ocst-%x61-7a-nat abnf::cst) 122)))
  :rule-classes :linear)

Theorem: ocst-"$"-leafterm

(defthm |OCST-"$"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"$\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"("-leafterm

(defthm |OCST-"("-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"(\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-")"-leafterm

(defthm |OCST-")"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\")\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-","-leafterm

(defthm |OCST-","-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\",\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"->"-leafterm

(defthm |OCST-"->"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"->\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"."-leafterm

(defthm |OCST-"."-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\".\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-":"-leafterm

(defthm |OCST-":"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\":\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-":="-leafterm

(defthm |OCST-":="-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\":=\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"\"-leafterm

(defthm |OCST-"\\"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"\\\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"_"-leafterm

(defthm |OCST-"_"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"_\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"{"-leafterm

(defthm |OCST-"{"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"{\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-"}"-leafterm

(defthm |OCST-"}"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "\"}\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%i"a"-leafterm

(defthm |OCST-%i"a"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%i\"a\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%i"b"-leafterm

(defthm |OCST-%i"b"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%i\"b\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%i"c"-leafterm

(defthm |OCST-%i"c"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%i\"c\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%i"d"-leafterm

(defthm |OCST-%i"d"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%i\"d\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%i"e"-leafterm

(defthm |OCST-%i"e"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%i\"e\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%i"f"-leafterm

(defthm |OCST-%i"f"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%i\"f\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"0x"-leafterm

(defthm |OCST-%s"0x"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"0x\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"break"-leafterm

(defthm |OCST-%s"break"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"break\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"case"-leafterm

(defthm |OCST-%s"case"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"case\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"continue"-leafterm

(defthm |OCST-%s"continue"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"continue\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"default"-leafterm

(defthm |OCST-%s"default"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"default\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"false"-leafterm

(defthm |OCST-%s"false"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"false\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"for"-leafterm

(defthm |OCST-%s"for"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"for\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"function"-leafterm

(defthm |OCST-%s"function"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"function\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"if"-leafterm

(defthm |OCST-%s"if"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"if\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"leave"-leafterm

(defthm |OCST-%s"leave"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"leave\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"let"-leafterm

(defthm |OCST-%s"let"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"let\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"switch"-leafterm

(defthm |OCST-%s"switch"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"switch\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-%s"true"-leafterm

(defthm |OCST-%s"true"-LEAFTERM|
  (implies (ocst-matchp abnf::cst "%s\"true\"")
           (equal (abnf::tree-kind abnf::cst)
                  :leafterm)))

Theorem: ocst-block-nonleaf

(defthm ocst-block-nonleaf
  (implies (ocst-matchp abnf::cst "block")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-statement-nonleaf

(defthm ocst-statement-nonleaf
  (implies (ocst-matchp abnf::cst "statement")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-functiondefinition-nonleaf

(defthm ocst-functiondefinition-nonleaf
  (implies (ocst-matchp abnf::cst "functiondefinition")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-variabledeclaration-nonleaf

(defthm ocst-variabledeclaration-nonleaf
  (implies (ocst-matchp abnf::cst "variabledeclaration")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-assignment-nonleaf

(defthm ocst-assignment-nonleaf
  (implies (ocst-matchp abnf::cst "assignment")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-expression-nonleaf

(defthm ocst-expression-nonleaf
  (implies (ocst-matchp abnf::cst "expression")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-if-nonleaf

(defthm ocst-if-nonleaf
  (implies (ocst-matchp abnf::cst "if")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-switch-nonleaf

(defthm ocst-switch-nonleaf
  (implies (ocst-matchp abnf::cst "switch")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-case-nonleaf

(defthm ocst-case-nonleaf
  (implies (ocst-matchp abnf::cst "case")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-default-nonleaf

(defthm ocst-default-nonleaf
  (implies (ocst-matchp abnf::cst "default")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-forloop-nonleaf

(defthm ocst-forloop-nonleaf
  (implies (ocst-matchp abnf::cst "forloop")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-breakcontinue-nonleaf

(defthm ocst-breakcontinue-nonleaf
  (implies (ocst-matchp abnf::cst "breakcontinue")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-leave-nonleaf

(defthm ocst-leave-nonleaf
  (implies (ocst-matchp abnf::cst "leave")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-functioncall-nonleaf

(defthm ocst-functioncall-nonleaf
  (implies (ocst-matchp abnf::cst "functioncall")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-lowercaseletter-nonleaf

(defthm ocst-lowercaseletter-nonleaf
  (implies (ocst-matchp abnf::cst "lowercaseletter")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-uppercaseletter-nonleaf

(defthm ocst-uppercaseletter-nonleaf
  (implies (ocst-matchp abnf::cst "uppercaseletter")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-identifierstart-nonleaf

(defthm ocst-identifierstart-nonleaf
  (implies (ocst-matchp abnf::cst "identifierstart")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-identifierrest-nonleaf

(defthm ocst-identifierrest-nonleaf
  (implies (ocst-matchp abnf::cst "identifierrest")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-identifier-nonleaf

(defthm ocst-identifier-nonleaf
  (implies (ocst-matchp abnf::cst "identifier")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-identifierlist-nonleaf

(defthm ocst-identifierlist-nonleaf
  (implies (ocst-matchp abnf::cst "identifierlist")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-typename-nonleaf

(defthm ocst-typename-nonleaf
  (implies (ocst-matchp abnf::cst "typename")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-typedidentifierlist-nonleaf

(defthm ocst-typedidentifierlist-nonleaf
  (implies (ocst-matchp abnf::cst "typedidentifierlist")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-literal-nonleaf

(defthm ocst-literal-nonleaf
  (implies (ocst-matchp abnf::cst "literal")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-numberliteral-nonleaf

(defthm ocst-numberliteral-nonleaf
  (implies (ocst-matchp abnf::cst "numberliteral")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-dquote-nonleaf

(defthm ocst-dquote-nonleaf
  (implies (ocst-matchp abnf::cst "dquote")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-not-dquote-cr-lf-nonleaf

(defthm ocst-not-dquote-cr-lf-nonleaf
  (implies (ocst-matchp abnf::cst "not-dquote-cr-lf")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-any-nonleaf

(defthm ocst-any-nonleaf
  (implies (ocst-matchp abnf::cst "any")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-stringliteral-nonleaf

(defthm ocst-stringliteral-nonleaf
  (implies (ocst-matchp abnf::cst "stringliteral")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-trueliteral-nonleaf

(defthm ocst-trueliteral-nonleaf
  (implies (ocst-matchp abnf::cst "trueliteral")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-falseliteral-nonleaf

(defthm ocst-falseliteral-nonleaf
  (implies (ocst-matchp abnf::cst "falseliteral")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-decimaldigit-nonleaf

(defthm ocst-decimaldigit-nonleaf
  (implies (ocst-matchp abnf::cst "decimaldigit")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-hexdigit-nonleaf

(defthm ocst-hexdigit-nonleaf
  (implies (ocst-matchp abnf::cst "hexdigit")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-hexnumber-nonleaf

(defthm ocst-hexnumber-nonleaf
  (implies (ocst-matchp abnf::cst "hexnumber")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-decimalnumber-nonleaf

(defthm ocst-decimalnumber-nonleaf
  (implies (ocst-matchp abnf::cst "decimalnumber")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: ocst-block-rulename

(defthm ocst-block-rulename
  (implies (ocst-matchp abnf::cst "block")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "block"))))

Theorem: ocst-statement-rulename

(defthm ocst-statement-rulename
  (implies (ocst-matchp abnf::cst "statement")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "statement"))))

Theorem: ocst-functiondefinition-rulename

(defthm ocst-functiondefinition-rulename
  (implies (ocst-matchp abnf::cst "functiondefinition")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "functiondefinition"))))

Theorem: ocst-variabledeclaration-rulename

(defthm ocst-variabledeclaration-rulename
  (implies (ocst-matchp abnf::cst "variabledeclaration")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "variabledeclaration"))))

Theorem: ocst-assignment-rulename

(defthm ocst-assignment-rulename
  (implies (ocst-matchp abnf::cst "assignment")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "assignment"))))

Theorem: ocst-expression-rulename

(defthm ocst-expression-rulename
  (implies (ocst-matchp abnf::cst "expression")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "expression"))))

Theorem: ocst-if-rulename

(defthm ocst-if-rulename
  (implies (ocst-matchp abnf::cst "if")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "if"))))

Theorem: ocst-switch-rulename

(defthm ocst-switch-rulename
  (implies (ocst-matchp abnf::cst "switch")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "switch"))))

Theorem: ocst-case-rulename

(defthm ocst-case-rulename
  (implies (ocst-matchp abnf::cst "case")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "case"))))

Theorem: ocst-default-rulename

(defthm ocst-default-rulename
  (implies (ocst-matchp abnf::cst "default")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "default"))))

Theorem: ocst-forloop-rulename

(defthm ocst-forloop-rulename
  (implies (ocst-matchp abnf::cst "forloop")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "forloop"))))

Theorem: ocst-breakcontinue-rulename

(defthm ocst-breakcontinue-rulename
  (implies (ocst-matchp abnf::cst "breakcontinue")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "breakcontinue"))))

Theorem: ocst-leave-rulename

(defthm ocst-leave-rulename
  (implies (ocst-matchp abnf::cst "leave")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "leave"))))

Theorem: ocst-functioncall-rulename

(defthm ocst-functioncall-rulename
  (implies (ocst-matchp abnf::cst "functioncall")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "functioncall"))))

Theorem: ocst-lowercaseletter-rulename

(defthm ocst-lowercaseletter-rulename
  (implies (ocst-matchp abnf::cst "lowercaseletter")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "lowercaseletter"))))

Theorem: ocst-uppercaseletter-rulename

(defthm ocst-uppercaseletter-rulename
  (implies (ocst-matchp abnf::cst "uppercaseletter")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "uppercaseletter"))))

Theorem: ocst-identifierstart-rulename

(defthm ocst-identifierstart-rulename
  (implies (ocst-matchp abnf::cst "identifierstart")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "identifierstart"))))

Theorem: ocst-identifierrest-rulename

(defthm ocst-identifierrest-rulename
  (implies (ocst-matchp abnf::cst "identifierrest")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "identifierrest"))))

Theorem: ocst-identifier-rulename

(defthm ocst-identifier-rulename
  (implies (ocst-matchp abnf::cst "identifier")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "identifier"))))

Theorem: ocst-identifierlist-rulename

(defthm ocst-identifierlist-rulename
  (implies (ocst-matchp abnf::cst "identifierlist")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "identifierlist"))))

Theorem: ocst-typename-rulename

(defthm ocst-typename-rulename
  (implies (ocst-matchp abnf::cst "typename")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "typename"))))

Theorem: ocst-typedidentifierlist-rulename

(defthm ocst-typedidentifierlist-rulename
  (implies (ocst-matchp abnf::cst "typedidentifierlist")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "typedidentifierlist"))))

Theorem: ocst-literal-rulename

(defthm ocst-literal-rulename
  (implies (ocst-matchp abnf::cst "literal")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "literal"))))

Theorem: ocst-numberliteral-rulename

(defthm ocst-numberliteral-rulename
  (implies (ocst-matchp abnf::cst "numberliteral")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "numberliteral"))))

Theorem: ocst-dquote-rulename

(defthm ocst-dquote-rulename
  (implies (ocst-matchp abnf::cst "dquote")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "dquote"))))

Theorem: ocst-not-dquote-cr-lf-rulename

(defthm ocst-not-dquote-cr-lf-rulename
  (implies (ocst-matchp abnf::cst "not-dquote-cr-lf")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "not-dquote-cr-lf"))))

Theorem: ocst-any-rulename

(defthm ocst-any-rulename
  (implies (ocst-matchp abnf::cst "any")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "any"))))

Theorem: ocst-stringliteral-rulename

(defthm ocst-stringliteral-rulename
  (implies (ocst-matchp abnf::cst "stringliteral")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "stringliteral"))))

Theorem: ocst-trueliteral-rulename

(defthm ocst-trueliteral-rulename
  (implies (ocst-matchp abnf::cst "trueliteral")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "trueliteral"))))

Theorem: ocst-falseliteral-rulename

(defthm ocst-falseliteral-rulename
  (implies (ocst-matchp abnf::cst "falseliteral")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "falseliteral"))))

Theorem: ocst-decimaldigit-rulename

(defthm ocst-decimaldigit-rulename
  (implies (ocst-matchp abnf::cst "decimaldigit")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "decimaldigit"))))

Theorem: ocst-hexdigit-rulename

(defthm ocst-hexdigit-rulename
  (implies (ocst-matchp abnf::cst "hexdigit")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "hexdigit"))))

Theorem: ocst-hexnumber-rulename

(defthm ocst-hexnumber-rulename
  (implies (ocst-matchp abnf::cst "hexnumber")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "hexnumber"))))

Theorem: ocst-decimalnumber-rulename

(defthm ocst-decimalnumber-rulename
  (implies (ocst-matchp abnf::cst "decimalnumber")
           (equal (abnf::tree-nonleaf->rulename? abnf::cst)
                  (abnf::rulename "decimalnumber"))))

Theorem: ocst-block-branches-match-alt

(defthm ocst-block-branches-match-alt
  (implies (ocst-matchp abnf::cst "block")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "\"{\" *statement \"}\"")))

Theorem: ocst-statement-branches-match-alt

(defthm ocst-statement-branches-match-alt
 (implies
  (ocst-matchp abnf::cst "statement")
  (ocst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "block / functiondefinition / variabledeclaration / assignment / if / expression / switch / forloop / breakcontinue / leave")))

Theorem: ocst-functiondefinition-branches-match-alt

(defthm ocst-functiondefinition-branches-match-alt
 (implies
  (ocst-matchp abnf::cst "functiondefinition")
  (ocst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "%s\"function\" identifier \"(\" [ typedidentifierlist ] \")\" [ \"->\" typedidentifierlist ] block")))

Theorem: ocst-variabledeclaration-branches-match-alt

(defthm ocst-variabledeclaration-branches-match-alt
  (implies (ocst-matchp abnf::cst "variabledeclaration")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"let\" typedidentifierlist [ \":=\" expression ]")))

Theorem: ocst-assignment-branches-match-alt

(defthm ocst-assignment-branches-match-alt
  (implies (ocst-matchp abnf::cst "assignment")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "identifierlist \":=\" expression")))

Theorem: ocst-expression-branches-match-alt

(defthm ocst-expression-branches-match-alt
  (implies (ocst-matchp abnf::cst "expression")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "functioncall / identifier / literal")))

Theorem: ocst-if-branches-match-alt

(defthm ocst-if-branches-match-alt
  (implies (ocst-matchp abnf::cst "if")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"if\" expression block")))

Theorem: ocst-switch-branches-match-alt

(defthm ocst-switch-branches-match-alt
 (implies
    (ocst-matchp abnf::cst "switch")
    (ocst-list-list-alt-matchp
         (abnf::tree-nonleaf->branches abnf::cst)
         "%s\"switch\" expression ( 1*case [ default ] / default )")))

Theorem: ocst-case-branches-match-alt

(defthm ocst-case-branches-match-alt
  (implies (ocst-matchp abnf::cst "case")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"case\" literal block")))

Theorem: ocst-default-branches-match-alt

(defthm ocst-default-branches-match-alt
  (implies (ocst-matchp abnf::cst "default")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"default\" block")))

Theorem: ocst-forloop-branches-match-alt

(defthm ocst-forloop-branches-match-alt
  (implies (ocst-matchp abnf::cst "forloop")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"for\" block expression block block")))

Theorem: ocst-breakcontinue-branches-match-alt

(defthm ocst-breakcontinue-branches-match-alt
  (implies (ocst-matchp abnf::cst "breakcontinue")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"break\" / %s\"continue\"")))

Theorem: ocst-leave-branches-match-alt

(defthm ocst-leave-branches-match-alt
  (implies (ocst-matchp abnf::cst "leave")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"leave\"")))

Theorem: ocst-functioncall-branches-match-alt

(defthm ocst-functioncall-branches-match-alt
 (implies
     (ocst-matchp abnf::cst "functioncall")
     (ocst-list-list-alt-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "identifier \"(\" [ expression *( \",\" expression ) ] \")\"")))

Theorem: ocst-lowercaseletter-branches-match-alt

(defthm ocst-lowercaseletter-branches-match-alt
  (implies (ocst-matchp abnf::cst "lowercaseletter")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%x61-7A")))

Theorem: ocst-uppercaseletter-branches-match-alt

(defthm ocst-uppercaseletter-branches-match-alt
  (implies (ocst-matchp abnf::cst "uppercaseletter")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%x41-5A")))

Theorem: ocst-identifierstart-branches-match-alt

(defthm ocst-identifierstart-branches-match-alt
  (implies (ocst-matchp abnf::cst "identifierstart")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "lowercaseletter / uppercaseletter / \"_\" / \"$\"")))

Theorem: ocst-identifierrest-branches-match-alt

(defthm ocst-identifierrest-branches-match-alt
  (implies (ocst-matchp abnf::cst "identifierrest")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "identifierstart / decimaldigit / \".\"")))

Theorem: ocst-identifier-branches-match-alt

(defthm ocst-identifier-branches-match-alt
  (implies (ocst-matchp abnf::cst "identifier")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "identifierstart *identifierrest")))

Theorem: ocst-identifierlist-branches-match-alt

(defthm ocst-identifierlist-branches-match-alt
  (implies (ocst-matchp abnf::cst "identifierlist")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "identifier *( \",\" identifier )")))

Theorem: ocst-typename-branches-match-alt

(defthm ocst-typename-branches-match-alt
  (implies (ocst-matchp abnf::cst "typename")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "identifier")))

Theorem: ocst-typedidentifierlist-branches-match-alt

(defthm ocst-typedidentifierlist-branches-match-alt
 (implies
  (ocst-matchp abnf::cst "typedidentifierlist")
  (ocst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "identifier [ \":\" typename ] *( \",\" identifier [ \":\" typename ] )")))

Theorem: ocst-literal-branches-match-alt

(defthm ocst-literal-branches-match-alt
 (implies
  (ocst-matchp abnf::cst "literal")
  (ocst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "( numberliteral / stringliteral / trueliteral / falseliteral ) [ \":\" typename ]")))

Theorem: ocst-numberliteral-branches-match-alt

(defthm ocst-numberliteral-branches-match-alt
  (implies (ocst-matchp abnf::cst "numberliteral")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "hexnumber / decimalnumber")))

Theorem: ocst-dquote-branches-match-alt

(defthm ocst-dquote-branches-match-alt
  (implies (ocst-matchp abnf::cst "dquote")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%x22")))

Theorem: ocst-not-dquote-cr-lf-branches-match-alt

(defthm ocst-not-dquote-cr-lf-branches-match-alt
  (implies (ocst-matchp abnf::cst "not-dquote-cr-lf")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%x0-9 / %xB-C / %xE-21 / %x23-5B / %x5D-10FFFF")))

Theorem: ocst-any-branches-match-alt

(defthm ocst-any-branches-match-alt
  (implies (ocst-matchp abnf::cst "any")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%x0-10FFFF")))

Theorem: ocst-stringliteral-branches-match-alt

(defthm ocst-stringliteral-branches-match-alt
  (implies (ocst-matchp abnf::cst "stringliteral")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "dquote *( not-dquote-cr-lf / \"\\\" any ) dquote")))

Theorem: ocst-trueliteral-branches-match-alt

(defthm ocst-trueliteral-branches-match-alt
  (implies (ocst-matchp abnf::cst "trueliteral")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"true\"")))

Theorem: ocst-falseliteral-branches-match-alt

(defthm ocst-falseliteral-branches-match-alt
  (implies (ocst-matchp abnf::cst "falseliteral")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"false\"")))

Theorem: ocst-decimaldigit-branches-match-alt

(defthm ocst-decimaldigit-branches-match-alt
  (implies (ocst-matchp abnf::cst "decimaldigit")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%x30-39")))

Theorem: ocst-hexdigit-branches-match-alt

(defthm ocst-hexdigit-branches-match-alt
 (implies
  (ocst-matchp abnf::cst "hexdigit")
  (ocst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "decimaldigit / %i\"a\" / %i\"b\" / %i\"c\" / %i\"d\" / %i\"e\" / %i\"f\"")))

Theorem: ocst-hexnumber-branches-match-alt

(defthm ocst-hexnumber-branches-match-alt
  (implies (ocst-matchp abnf::cst "hexnumber")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "%s\"0x\" 1*hexdigit")))

Theorem: ocst-decimalnumber-branches-match-alt

(defthm ocst-decimalnumber-branches-match-alt
  (implies (ocst-matchp abnf::cst "decimalnumber")
           (ocst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "1*decimaldigit")))

Theorem: ocst-block-concs

(defthm ocst-block-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss "\"{\" *statement \"}\"")
  (or
    (ocst-list-list-conc-matchp abnf::cstss "\"{\" *statement \"}\""))))

Theorem: ocst-statement-concs

(defthm ocst-statement-concs
 (implies
  (ocst-list-list-alt-matchp
   abnf::cstss
   "block / functiondefinition / variabledeclaration / assignment / if / expression / switch / forloop / breakcontinue / leave")
  (or (ocst-list-list-conc-matchp abnf::cstss "block")
      (ocst-list-list-conc-matchp abnf::cstss "functiondefinition")
      (ocst-list-list-conc-matchp abnf::cstss "variabledeclaration")
      (ocst-list-list-conc-matchp abnf::cstss "assignment")
      (ocst-list-list-conc-matchp abnf::cstss "if")
      (ocst-list-list-conc-matchp abnf::cstss "expression")
      (ocst-list-list-conc-matchp abnf::cstss "switch")
      (ocst-list-list-conc-matchp abnf::cstss "forloop")
      (ocst-list-list-conc-matchp abnf::cstss "breakcontinue")
      (ocst-list-list-conc-matchp abnf::cstss "leave"))))

Theorem: ocst-functiondefinition-concs

(defthm ocst-functiondefinition-concs
 (implies
  (ocst-list-list-alt-matchp
   abnf::cstss
   "%s\"function\" identifier \"(\" [ typedidentifierlist ] \")\" [ \"->\" typedidentifierlist ] block")
  (or
   (ocst-list-list-conc-matchp
    abnf::cstss
    "%s\"function\" identifier \"(\" [ typedidentifierlist ] \")\" [ \"->\" typedidentifierlist ] block"))))

Theorem: ocst-variabledeclaration-concs

(defthm ocst-variabledeclaration-concs
 (implies
      (ocst-list-list-alt-matchp
           abnf::cstss
           "%s\"let\" typedidentifierlist [ \":=\" expression ]")
      (or (ocst-list-list-conc-matchp
               abnf::cstss
               "%s\"let\" typedidentifierlist [ \":=\" expression ]"))))

Theorem: ocst-assignment-concs

(defthm ocst-assignment-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss
                             "identifierlist \":=\" expression")
  (or
    (ocst-list-list-conc-matchp abnf::cstss
                                "identifierlist \":=\" expression"))))

Theorem: ocst-expression-concs

(defthm ocst-expression-concs
 (implies
   (ocst-list-list-alt-matchp abnf::cstss
                              "functioncall / identifier / literal")
   (or (ocst-list-list-conc-matchp abnf::cstss "functioncall")
       (ocst-list-list-conc-matchp abnf::cstss "identifier")
       (ocst-list-list-conc-matchp abnf::cstss "literal"))))

Theorem: ocst-if-concs

(defthm ocst-if-concs
 (implies
   (ocst-list-list-alt-matchp abnf::cstss "%s\"if\" expression block")
   (or (ocst-list-list-conc-matchp abnf::cstss
                                   "%s\"if\" expression block"))))

Theorem: ocst-switch-concs

(defthm ocst-switch-concs
 (implies
  (ocst-list-list-alt-matchp
       abnf::cstss
       "%s\"switch\" expression ( 1*case [ default ] / default )")
  (or
   (ocst-list-list-conc-matchp
        abnf::cstss
        "%s\"switch\" expression ( 1*case [ default ] / default )"))))

Theorem: ocst-case-concs

(defthm ocst-case-concs
 (implies
    (ocst-list-list-alt-matchp abnf::cstss "%s\"case\" literal block")
    (or (ocst-list-list-conc-matchp
             abnf::cstss "%s\"case\" literal block"))))

Theorem: ocst-default-concs

(defthm ocst-default-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss "%s\"default\" block")
  (or
     (ocst-list-list-conc-matchp abnf::cstss "%s\"default\" block"))))

Theorem: ocst-forloop-concs

(defthm ocst-forloop-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss
                             "%s\"for\" block expression block block")
  (or (ocst-list-list-conc-matchp
           abnf::cstss
           "%s\"for\" block expression block block"))))

Theorem: ocst-breakcontinue-concs

(defthm ocst-breakcontinue-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss "%s\"break\" / %s\"continue\"")
  (or (ocst-list-list-conc-matchp abnf::cstss "%s\"break\"")
      (ocst-list-list-conc-matchp abnf::cstss "%s\"continue\""))))

Theorem: ocst-leave-concs

(defthm ocst-leave-concs
  (implies
       (ocst-list-list-alt-matchp abnf::cstss "%s\"leave\"")
       (or (ocst-list-list-conc-matchp abnf::cstss "%s\"leave\""))))

Theorem: ocst-functioncall-concs

(defthm ocst-functioncall-concs
 (implies
  (ocst-list-list-alt-matchp
       abnf::cstss
       "identifier \"(\" [ expression *( \",\" expression ) ] \")\"")
  (or
    (ocst-list-list-conc-matchp
         abnf::cstss
         "identifier \"(\" [ expression *( \",\" expression ) ] \")\""))))

Theorem: ocst-lowercaseletter-concs

(defthm ocst-lowercaseletter-concs
  (implies (ocst-list-list-alt-matchp abnf::cstss "%x61-7A")
           (or (ocst-list-list-conc-matchp abnf::cstss "%x61-7A"))))

Theorem: ocst-uppercaseletter-concs

(defthm ocst-uppercaseletter-concs
  (implies (ocst-list-list-alt-matchp abnf::cstss "%x41-5A")
           (or (ocst-list-list-conc-matchp abnf::cstss "%x41-5A"))))

Theorem: ocst-identifierstart-concs

(defthm ocst-identifierstart-concs
 (implies
      (ocst-list-list-alt-matchp
           abnf::cstss
           "lowercaseletter / uppercaseletter / \"_\" / \"$\"")
      (or (ocst-list-list-conc-matchp abnf::cstss "lowercaseletter")
          (ocst-list-list-conc-matchp abnf::cstss "uppercaseletter")
          (ocst-list-list-conc-matchp abnf::cstss "\"_\"")
          (ocst-list-list-conc-matchp abnf::cstss "\"$\""))))

Theorem: ocst-identifierrest-concs

(defthm ocst-identifierrest-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss
                             "identifierstart / decimaldigit / \".\"")
  (or (ocst-list-list-conc-matchp abnf::cstss "identifierstart")
      (ocst-list-list-conc-matchp abnf::cstss "decimaldigit")
      (ocst-list-list-conc-matchp abnf::cstss "\".\""))))

Theorem: ocst-identifier-concs

(defthm ocst-identifier-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss
                             "identifierstart *identifierrest")
  (or
   (ocst-list-list-conc-matchp abnf::cstss
                               "identifierstart *identifierrest"))))

Theorem: ocst-identifierlist-concs

(defthm ocst-identifierlist-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss
                             "identifier *( \",\" identifier )")
  (or
    (ocst-list-list-conc-matchp abnf::cstss
                                "identifier *( \",\" identifier )"))))

Theorem: ocst-typename-concs

(defthm ocst-typename-concs
  (implies
       (ocst-list-list-alt-matchp abnf::cstss "identifier")
       (or (ocst-list-list-conc-matchp abnf::cstss "identifier"))))

Theorem: ocst-typedidentifierlist-concs

(defthm ocst-typedidentifierlist-concs
 (implies
  (ocst-list-list-alt-matchp
   abnf::cstss
   "identifier [ \":\" typename ] *( \",\" identifier [ \":\" typename ] )")
  (or
   (ocst-list-list-conc-matchp
    abnf::cstss
    "identifier [ \":\" typename ] *( \",\" identifier [ \":\" typename ] )"))))

Theorem: ocst-literal-concs

(defthm ocst-literal-concs
 (implies
  (ocst-list-list-alt-matchp
   abnf::cstss
   "( numberliteral / stringliteral / trueliteral / falseliteral ) [ \":\" typename ]")
  (or
   (ocst-list-list-conc-matchp
    abnf::cstss
    "( numberliteral / stringliteral / trueliteral / falseliteral ) [ \":\" typename ]"))))

Theorem: ocst-numberliteral-concs

(defthm ocst-numberliteral-concs
 (implies
     (ocst-list-list-alt-matchp
          abnf::cstss "hexnumber / decimalnumber")
     (or (ocst-list-list-conc-matchp abnf::cstss "hexnumber")
         (ocst-list-list-conc-matchp abnf::cstss "decimalnumber"))))

Theorem: ocst-dquote-concs

(defthm ocst-dquote-concs
  (implies (ocst-list-list-alt-matchp abnf::cstss "%x22")
           (or (ocst-list-list-conc-matchp abnf::cstss "%x22"))))

Theorem: ocst-not-dquote-cr-lf-concs

(defthm ocst-not-dquote-cr-lf-concs
  (implies
       (ocst-list-list-alt-matchp
            abnf::cstss
            "%x0-9 / %xB-C / %xE-21 / %x23-5B / %x5D-10FFFF")
       (or (ocst-list-list-conc-matchp abnf::cstss "%x0-9")
           (ocst-list-list-conc-matchp abnf::cstss "%xB-C")
           (ocst-list-list-conc-matchp abnf::cstss "%xE-21")
           (ocst-list-list-conc-matchp abnf::cstss "%x23-5B")
           (ocst-list-list-conc-matchp abnf::cstss "%x5D-10FFFF"))))

Theorem: ocst-any-concs

(defthm ocst-any-concs
  (implies
       (ocst-list-list-alt-matchp abnf::cstss "%x0-10FFFF")
       (or (ocst-list-list-conc-matchp abnf::cstss "%x0-10FFFF"))))

Theorem: ocst-stringliteral-concs

(defthm ocst-stringliteral-concs
  (implies
       (ocst-list-list-alt-matchp
            abnf::cstss
            "dquote *( not-dquote-cr-lf / \"\\\" any ) dquote")
       (or (ocst-list-list-conc-matchp
                abnf::cstss
                "dquote *( not-dquote-cr-lf / \"\\\" any ) dquote"))))

Theorem: ocst-trueliteral-concs

(defthm ocst-trueliteral-concs
 (implies (ocst-list-list-alt-matchp abnf::cstss "%s\"true\"")
          (or (ocst-list-list-conc-matchp abnf::cstss "%s\"true\""))))

Theorem: ocst-falseliteral-concs

(defthm ocst-falseliteral-concs
  (implies
       (ocst-list-list-alt-matchp abnf::cstss "%s\"false\"")
       (or (ocst-list-list-conc-matchp abnf::cstss "%s\"false\""))))

Theorem: ocst-decimaldigit-concs

(defthm ocst-decimaldigit-concs
  (implies (ocst-list-list-alt-matchp abnf::cstss "%x30-39")
           (or (ocst-list-list-conc-matchp abnf::cstss "%x30-39"))))

Theorem: ocst-hexdigit-concs

(defthm ocst-hexdigit-concs
 (implies
  (ocst-list-list-alt-matchp
     abnf::cstss
     "decimaldigit / %i\"a\" / %i\"b\" / %i\"c\" / %i\"d\" / %i\"e\" / %i\"f\"")
  (or (ocst-list-list-conc-matchp abnf::cstss "decimaldigit")
      (ocst-list-list-conc-matchp abnf::cstss "%i\"a\"")
      (ocst-list-list-conc-matchp abnf::cstss "%i\"b\"")
      (ocst-list-list-conc-matchp abnf::cstss "%i\"c\"")
      (ocst-list-list-conc-matchp abnf::cstss "%i\"d\"")
      (ocst-list-list-conc-matchp abnf::cstss "%i\"e\"")
      (ocst-list-list-conc-matchp abnf::cstss "%i\"f\""))))

Theorem: ocst-hexnumber-concs

(defthm ocst-hexnumber-concs
 (implies
  (ocst-list-list-alt-matchp abnf::cstss "%s\"0x\" 1*hexdigit")
  (or
     (ocst-list-list-conc-matchp abnf::cstss "%s\"0x\" 1*hexdigit"))))

Theorem: ocst-decimalnumber-concs

(defthm ocst-decimalnumber-concs
 (implies
    (ocst-list-list-alt-matchp abnf::cstss "1*decimaldigit")
    (or (ocst-list-list-conc-matchp abnf::cstss "1*decimaldigit"))))

Theorem: ocst-statement-conc1-matching

(defthm ocst-statement-conc1-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "block")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "block"))))

Theorem: ocst-statement-conc2-matching

(defthm ocst-statement-conc2-matching
  (implies
       (ocst-list-list-conc-matchp abnf::cstss "functiondefinition")
       (and (equal (len abnf::cstss) 1)
            (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                  "functiondefinition"))))

Theorem: ocst-statement-conc3-matching

(defthm ocst-statement-conc3-matching
 (implies
      (ocst-list-list-conc-matchp abnf::cstss "variabledeclaration")
      (and (equal (len abnf::cstss) 1)
           (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                 "variabledeclaration"))))

Theorem: ocst-statement-conc4-matching

(defthm ocst-statement-conc4-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "assignment")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "assignment"))))

Theorem: ocst-statement-conc5-matching

(defthm ocst-statement-conc5-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "if")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "if"))))

Theorem: ocst-statement-conc6-matching

(defthm ocst-statement-conc6-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "expression")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "expression"))))

Theorem: ocst-statement-conc7-matching

(defthm ocst-statement-conc7-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "switch")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "switch"))))

Theorem: ocst-statement-conc8-matching

(defthm ocst-statement-conc8-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "forloop")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "forloop"))))

Theorem: ocst-statement-conc9-matching

(defthm ocst-statement-conc9-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "breakcontinue")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "breakcontinue"))))

Theorem: ocst-statement-conc10-matching

(defthm ocst-statement-conc10-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "leave")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "leave"))))

Theorem: ocst-expression-conc1-matching

(defthm ocst-expression-conc1-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "functioncall")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "functioncall"))))

Theorem: ocst-expression-conc2-matching

(defthm ocst-expression-conc2-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "identifier")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "identifier"))))

Theorem: ocst-expression-conc3-matching

(defthm ocst-expression-conc3-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "literal")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "literal"))))

Theorem: ocst-breakcontinue-conc1-matching

(defthm ocst-breakcontinue-conc1-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%s\"break\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%s\"break\""))))

Theorem: ocst-breakcontinue-conc2-matching

(defthm ocst-breakcontinue-conc2-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%s\"continue\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%s\"continue\""))))

Theorem: ocst-leave-conc-matching

(defthm ocst-leave-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%s\"leave\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%s\"leave\""))))

Theorem: ocst-lowercaseletter-conc-matching

(defthm ocst-lowercaseletter-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x61-7A")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x61-7A"))))

Theorem: ocst-uppercaseletter-conc-matching

(defthm ocst-uppercaseletter-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x41-5A")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x41-5A"))))

Theorem: ocst-identifierstart-conc1-matching

(defthm ocst-identifierstart-conc1-matching
 (implies (ocst-list-list-conc-matchp abnf::cstss "lowercaseletter")
          (and (equal (len abnf::cstss) 1)
               (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                     "lowercaseletter"))))

Theorem: ocst-identifierstart-conc2-matching

(defthm ocst-identifierstart-conc2-matching
 (implies (ocst-list-list-conc-matchp abnf::cstss "uppercaseletter")
          (and (equal (len abnf::cstss) 1)
               (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                     "uppercaseletter"))))

Theorem: ocst-identifierstart-conc3-matching

(defthm ocst-identifierstart-conc3-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "\"_\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "\"_\""))))

Theorem: ocst-identifierstart-conc4-matching

(defthm ocst-identifierstart-conc4-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "\"$\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "\"$\""))))

Theorem: ocst-identifierrest-conc1-matching

(defthm ocst-identifierrest-conc1-matching
 (implies (ocst-list-list-conc-matchp abnf::cstss "identifierstart")
          (and (equal (len abnf::cstss) 1)
               (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                     "identifierstart"))))

Theorem: ocst-identifierrest-conc2-matching

(defthm ocst-identifierrest-conc2-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "decimaldigit")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "decimaldigit"))))

Theorem: ocst-identifierrest-conc3-matching

(defthm ocst-identifierrest-conc3-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "\".\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "\".\""))))

Theorem: ocst-typename-conc-matching

(defthm ocst-typename-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "identifier")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "identifier"))))

Theorem: ocst-numberliteral-conc1-matching

(defthm ocst-numberliteral-conc1-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "hexnumber")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "hexnumber"))))

Theorem: ocst-numberliteral-conc2-matching

(defthm ocst-numberliteral-conc2-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "decimalnumber")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "decimalnumber"))))

Theorem: ocst-dquote-conc-matching

(defthm ocst-dquote-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x22")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x22"))))

Theorem: ocst-not-dquote-cr-lf-conc1-matching

(defthm ocst-not-dquote-cr-lf-conc1-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x0-9")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x0-9"))))

Theorem: ocst-not-dquote-cr-lf-conc2-matching

(defthm ocst-not-dquote-cr-lf-conc2-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%xB-C")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%xB-C"))))

Theorem: ocst-not-dquote-cr-lf-conc3-matching

(defthm ocst-not-dquote-cr-lf-conc3-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%xE-21")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%xE-21"))))

Theorem: ocst-not-dquote-cr-lf-conc4-matching

(defthm ocst-not-dquote-cr-lf-conc4-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x23-5B")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x23-5B"))))

Theorem: ocst-not-dquote-cr-lf-conc5-matching

(defthm ocst-not-dquote-cr-lf-conc5-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x5D-10FFFF")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x5D-10FFFF"))))

Theorem: ocst-any-conc-matching

(defthm ocst-any-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x0-10FFFF")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x0-10FFFF"))))

Theorem: ocst-trueliteral-conc-matching

(defthm ocst-trueliteral-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%s\"true\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%s\"true\""))))

Theorem: ocst-falseliteral-conc-matching

(defthm ocst-falseliteral-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%s\"false\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%s\"false\""))))

Theorem: ocst-decimaldigit-conc-matching

(defthm ocst-decimaldigit-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%x30-39")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%x30-39"))))

Theorem: ocst-hexdigit-conc1-matching

(defthm ocst-hexdigit-conc1-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "decimaldigit")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "decimaldigit"))))

Theorem: ocst-hexdigit-conc2-matching

(defthm ocst-hexdigit-conc2-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%i\"a\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%i\"a\""))))

Theorem: ocst-hexdigit-conc3-matching

(defthm ocst-hexdigit-conc3-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%i\"b\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%i\"b\""))))

Theorem: ocst-hexdigit-conc4-matching

(defthm ocst-hexdigit-conc4-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%i\"c\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%i\"c\""))))

Theorem: ocst-hexdigit-conc5-matching

(defthm ocst-hexdigit-conc5-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%i\"d\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%i\"d\""))))

Theorem: ocst-hexdigit-conc6-matching

(defthm ocst-hexdigit-conc6-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%i\"e\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%i\"e\""))))

Theorem: ocst-hexdigit-conc7-matching

(defthm ocst-hexdigit-conc7-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "%i\"f\"")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "%i\"f\""))))

Theorem: ocst-decimalnumber-conc-matching

(defthm ocst-decimalnumber-conc-matching
  (implies (ocst-list-list-conc-matchp abnf::cstss "1*decimaldigit")
           (and (equal (len abnf::cstss) 1)
                (ocst-list-rep-matchp (nth 0 abnf::cstss)
                                      "1*decimaldigit"))))

Theorem: ocst-statement-conc1-rep-matching

(defthm ocst-statement-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "block")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "block"))))

Theorem: ocst-statement-conc2-rep-matching

(defthm ocst-statement-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "functiondefinition")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "functiondefinition"))))

Theorem: ocst-statement-conc3-rep-matching

(defthm ocst-statement-conc3-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "variabledeclaration")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "variabledeclaration"))))

Theorem: ocst-statement-conc4-rep-matching

(defthm ocst-statement-conc4-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "assignment")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "assignment"))))

Theorem: ocst-statement-conc5-rep-matching

(defthm ocst-statement-conc5-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "if")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts) "if"))))

Theorem: ocst-statement-conc6-rep-matching

(defthm ocst-statement-conc6-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "expression")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "expression"))))

Theorem: ocst-statement-conc7-rep-matching

(defthm ocst-statement-conc7-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "switch")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "switch"))))

Theorem: ocst-statement-conc8-rep-matching

(defthm ocst-statement-conc8-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "forloop")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "forloop"))))

Theorem: ocst-statement-conc9-rep-matching

(defthm ocst-statement-conc9-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "breakcontinue")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "breakcontinue"))))

Theorem: ocst-statement-conc10-rep-matching

(defthm ocst-statement-conc10-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "leave")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "leave"))))

Theorem: ocst-expression-conc1-rep-matching

(defthm ocst-expression-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "functioncall")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "functioncall"))))

Theorem: ocst-expression-conc2-rep-matching

(defthm ocst-expression-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "identifier")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "identifier"))))

Theorem: ocst-expression-conc3-rep-matching

(defthm ocst-expression-conc3-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "literal")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "literal"))))

Theorem: ocst-breakcontinue-conc1-rep-matching

(defthm ocst-breakcontinue-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%s\"break\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%s\"break\""))))

Theorem: ocst-breakcontinue-conc2-rep-matching

(defthm ocst-breakcontinue-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%s\"continue\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%s\"continue\""))))

Theorem: ocst-leave-conc-rep-matching

(defthm ocst-leave-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%s\"leave\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%s\"leave\""))))

Theorem: ocst-lowercaseletter-conc-rep-matching

(defthm ocst-lowercaseletter-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x61-7A")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x61-7A"))))

Theorem: ocst-uppercaseletter-conc-rep-matching

(defthm ocst-uppercaseletter-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x41-5A")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x41-5A"))))

Theorem: ocst-identifierstart-conc1-rep-matching

(defthm ocst-identifierstart-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "lowercaseletter")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "lowercaseletter"))))

Theorem: ocst-identifierstart-conc2-rep-matching

(defthm ocst-identifierstart-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "uppercaseletter")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "uppercaseletter"))))

Theorem: ocst-identifierstart-conc3-rep-matching

(defthm ocst-identifierstart-conc3-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "\"_\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "\"_\""))))

Theorem: ocst-identifierstart-conc4-rep-matching

(defthm ocst-identifierstart-conc4-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "\"$\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "\"$\""))))

Theorem: ocst-identifierrest-conc1-rep-matching

(defthm ocst-identifierrest-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "identifierstart")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "identifierstart"))))

Theorem: ocst-identifierrest-conc2-rep-matching

(defthm ocst-identifierrest-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "decimaldigit")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "decimaldigit"))))

Theorem: ocst-identifierrest-conc3-rep-matching

(defthm ocst-identifierrest-conc3-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "\".\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "\".\""))))

Theorem: ocst-typename-conc-rep-matching

(defthm ocst-typename-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "identifier")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "identifier"))))

Theorem: ocst-numberliteral-conc1-rep-matching

(defthm ocst-numberliteral-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "hexnumber")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "hexnumber"))))

Theorem: ocst-numberliteral-conc2-rep-matching

(defthm ocst-numberliteral-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "decimalnumber")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "decimalnumber"))))

Theorem: ocst-dquote-conc-rep-matching

(defthm ocst-dquote-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x22")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x22"))))

Theorem: ocst-not-dquote-cr-lf-conc1-rep-matching

(defthm ocst-not-dquote-cr-lf-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x0-9")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x0-9"))))

Theorem: ocst-not-dquote-cr-lf-conc2-rep-matching

(defthm ocst-not-dquote-cr-lf-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%xB-C")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%xB-C"))))

Theorem: ocst-not-dquote-cr-lf-conc3-rep-matching

(defthm ocst-not-dquote-cr-lf-conc3-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%xE-21")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%xE-21"))))

Theorem: ocst-not-dquote-cr-lf-conc4-rep-matching

(defthm ocst-not-dquote-cr-lf-conc4-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x23-5B")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x23-5B"))))

Theorem: ocst-not-dquote-cr-lf-conc5-rep-matching

(defthm ocst-not-dquote-cr-lf-conc5-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x5D-10FFFF")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x5D-10FFFF"))))

Theorem: ocst-any-conc-rep-matching

(defthm ocst-any-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x0-10FFFF")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x0-10FFFF"))))

Theorem: ocst-trueliteral-conc-rep-matching

(defthm ocst-trueliteral-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%s\"true\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%s\"true\""))))

Theorem: ocst-falseliteral-conc-rep-matching

(defthm ocst-falseliteral-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%s\"false\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%s\"false\""))))

Theorem: ocst-decimaldigit-conc-rep-matching

(defthm ocst-decimaldigit-conc-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%x30-39")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%x30-39"))))

Theorem: ocst-hexdigit-conc1-rep-matching

(defthm ocst-hexdigit-conc1-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "decimaldigit")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "decimaldigit"))))

Theorem: ocst-hexdigit-conc2-rep-matching

(defthm ocst-hexdigit-conc2-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%i\"a\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%i\"a\""))))

Theorem: ocst-hexdigit-conc3-rep-matching

(defthm ocst-hexdigit-conc3-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%i\"b\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%i\"b\""))))

Theorem: ocst-hexdigit-conc4-rep-matching

(defthm ocst-hexdigit-conc4-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%i\"c\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%i\"c\""))))

Theorem: ocst-hexdigit-conc5-rep-matching

(defthm ocst-hexdigit-conc5-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%i\"d\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%i\"d\""))))

Theorem: ocst-hexdigit-conc6-rep-matching

(defthm ocst-hexdigit-conc6-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%i\"e\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%i\"e\""))))

Theorem: ocst-hexdigit-conc7-rep-matching

(defthm ocst-hexdigit-conc7-rep-matching
  (implies (ocst-list-rep-matchp abnf::csts "%i\"f\"")
           (and (equal (len abnf::csts) 1)
                (ocst-matchp (nth 0 abnf::csts)
                             "%i\"f\""))))

Theorem: ocst-statement-conc-equivs

(defthm ocst-statement-conc-equivs
 (implies
  (ocst-matchp abnf::cst "statement")
  (and
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "block")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "block")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "functiondefinition")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "functiondefinition")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "variabledeclaration")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "variabledeclaration")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "assignment")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "assignment")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "if")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "if")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "expression")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "expression")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "switch")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "switch")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "forloop")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "forloop")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "breakcontinue")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "breakcontinue")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "leave")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "leave"))))))

Theorem: ocst-expression-conc-equivs

(defthm ocst-expression-conc-equivs
 (implies
  (ocst-matchp abnf::cst "expression")
  (and
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "functioncall")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "functioncall")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "identifier")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "identifier")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "literal")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "literal"))))))

Theorem: ocst-numberliteral-conc-equivs

(defthm ocst-numberliteral-conc-equivs
 (implies
  (ocst-matchp abnf::cst "numberliteral")
  (and
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "hexnumber")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "hexnumber")))
   (iff
     (ocst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "decimalnumber")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "decimalnumber"))))))

Function: ocst-statement-conc?

(defun ocst-statement-conc? (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "statement")))
 (let ((__function__ 'ocst-statement-conc?))
  (declare (ignorable __function__))
  (cond
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "block"))
     1)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "functiondefinition"))
     2)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "variabledeclaration"))
     3)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "assignment"))
     4)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "if"))
     5)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "expression"))
     6)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "switch"))
     7)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "forloop"))
     8)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "breakcontinue"))
     9)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "leave"))
     10)
    (t (prog2$ (impossible) 1)))))

Theorem: posp-of-ocst-statement-conc?

(defthm posp-of-ocst-statement-conc?
  (b* ((number (ocst-statement-conc? abnf::cst)))
    (posp number))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc?-possibilities

(defthm ocst-statement-conc?-possibilities
  (b* ((number (ocst-statement-conc? abnf::cst)))
    (or (equal number 1)
        (equal number 2)
        (equal number 3)
        (equal number 4)
        (equal number 5)
        (equal number 6)
        (equal number 7)
        (equal number 8)
        (equal number 9)
        (equal number 10)))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((ocst-statement-conc? abnf::cst)))))

Theorem: ocst-statement-conc?-of-tree-fix-cst

(defthm ocst-statement-conc?-of-tree-fix-cst
  (equal (ocst-statement-conc? (abnf::tree-fix abnf::cst))
         (ocst-statement-conc? abnf::cst)))

Theorem: ocst-statement-conc?-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc?-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc? abnf::cst)
                  (ocst-statement-conc? cst-equiv)))
  :rule-classes :congruence)

Theorem: ocst-statement-conc?-1-iff-match-conc

(defthm ocst-statement-conc?-1-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       1)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "block"))))

Theorem: ocst-statement-conc?-2-iff-match-conc

(defthm ocst-statement-conc?-2-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       2)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "functiondefinition"))))

Theorem: ocst-statement-conc?-3-iff-match-conc

(defthm ocst-statement-conc?-3-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       3)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "variabledeclaration"))))

Theorem: ocst-statement-conc?-4-iff-match-conc

(defthm ocst-statement-conc?-4-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       4)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "assignment"))))

Theorem: ocst-statement-conc?-5-iff-match-conc

(defthm ocst-statement-conc?-5-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       5)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "if"))))

Theorem: ocst-statement-conc?-6-iff-match-conc

(defthm ocst-statement-conc?-6-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       6)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "expression"))))

Theorem: ocst-statement-conc?-7-iff-match-conc

(defthm ocst-statement-conc?-7-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       7)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "switch"))))

Theorem: ocst-statement-conc?-8-iff-match-conc

(defthm ocst-statement-conc?-8-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       8)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "forloop"))))

Theorem: ocst-statement-conc?-9-iff-match-conc

(defthm ocst-statement-conc?-9-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       9)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "breakcontinue"))))

Theorem: ocst-statement-conc?-10-iff-match-conc

(defthm ocst-statement-conc?-10-iff-match-conc
  (implies (ocst-matchp abnf::cst "statement")
           (iff (equal (ocst-statement-conc? abnf::cst)
                       10)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "leave"))))

Function: ocst-expression-conc?

(defun ocst-expression-conc? (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "expression")))
 (let ((__function__ 'ocst-expression-conc?))
  (declare (ignorable __function__))
  (cond
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "functioncall"))
     1)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "identifier"))
     2)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "literal"))
     3)
    (t (prog2$ (impossible) 1)))))

Theorem: posp-of-ocst-expression-conc?

(defthm posp-of-ocst-expression-conc?
  (b* ((number (ocst-expression-conc? abnf::cst)))
    (posp number))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc?-possibilities

(defthm ocst-expression-conc?-possibilities
  (b* ((number (ocst-expression-conc? abnf::cst)))
    (or (equal number 1)
        (equal number 2)
        (equal number 3)))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((ocst-expression-conc? abnf::cst)))))

Theorem: ocst-expression-conc?-of-tree-fix-cst

(defthm ocst-expression-conc?-of-tree-fix-cst
  (equal (ocst-expression-conc? (abnf::tree-fix abnf::cst))
         (ocst-expression-conc? abnf::cst)))

Theorem: ocst-expression-conc?-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc?-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc? abnf::cst)
                  (ocst-expression-conc? cst-equiv)))
  :rule-classes :congruence)

Theorem: ocst-expression-conc?-1-iff-match-conc

(defthm ocst-expression-conc?-1-iff-match-conc
  (implies (ocst-matchp abnf::cst "expression")
           (iff (equal (ocst-expression-conc? abnf::cst)
                       1)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "functioncall"))))

Theorem: ocst-expression-conc?-2-iff-match-conc

(defthm ocst-expression-conc?-2-iff-match-conc
  (implies (ocst-matchp abnf::cst "expression")
           (iff (equal (ocst-expression-conc? abnf::cst)
                       2)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "identifier"))))

Theorem: ocst-expression-conc?-3-iff-match-conc

(defthm ocst-expression-conc?-3-iff-match-conc
  (implies (ocst-matchp abnf::cst "expression")
           (iff (equal (ocst-expression-conc? abnf::cst)
                       3)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "literal"))))

Function: ocst-numberliteral-conc?

(defun ocst-numberliteral-conc? (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "numberliteral")))
 (let ((__function__ 'ocst-numberliteral-conc?))
  (declare (ignorable __function__))
  (cond
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "hexnumber"))
     1)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "decimalnumber"))
     2)
    (t (prog2$ (impossible) 1)))))

Theorem: posp-of-ocst-numberliteral-conc?

(defthm posp-of-ocst-numberliteral-conc?
  (b* ((number (ocst-numberliteral-conc? abnf::cst)))
    (posp number))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc?-possibilities

(defthm ocst-numberliteral-conc?-possibilities
  (b* ((number (ocst-numberliteral-conc? abnf::cst)))
    (or (equal number 1) (equal number 2)))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((ocst-numberliteral-conc? abnf::cst)))))

Theorem: ocst-numberliteral-conc?-of-tree-fix-cst

(defthm ocst-numberliteral-conc?-of-tree-fix-cst
  (equal (ocst-numberliteral-conc? (abnf::tree-fix abnf::cst))
         (ocst-numberliteral-conc? abnf::cst)))

Theorem: ocst-numberliteral-conc?-tree-equiv-congruence-on-cst

(defthm ocst-numberliteral-conc?-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc? abnf::cst)
                  (ocst-numberliteral-conc? cst-equiv)))
  :rule-classes :congruence)

Theorem: ocst-numberliteral-conc?-1-iff-match-conc

(defthm ocst-numberliteral-conc?-1-iff-match-conc
  (implies (ocst-matchp abnf::cst "numberliteral")
           (iff (equal (ocst-numberliteral-conc? abnf::cst)
                       1)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "hexnumber"))))

Theorem: ocst-numberliteral-conc?-2-iff-match-conc

(defthm ocst-numberliteral-conc?-2-iff-match-conc
  (implies (ocst-matchp abnf::cst "numberliteral")
           (iff (equal (ocst-numberliteral-conc? abnf::cst)
                       2)
                (ocst-list-list-conc-matchp
                     (abnf::tree-nonleaf->branches abnf::cst)
                     "decimalnumber"))))

Function: ocst-block-conc

(defun ocst-block-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "block")))
  (let ((__function__ 'ocst-block-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-block-conc

(defthm tree-list-listp-of-ocst-block-conc
  (b* ((abnf::cstss (ocst-block-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-block-conc-match

(defthm ocst-block-conc-match
 (implies
   (ocst-matchp abnf::cst "block")
   (b* ((abnf::cstss (ocst-block-conc abnf::cst)))
     (ocst-list-list-conc-matchp abnf::cstss "\"{\" *statement \"}\"")))
 :rule-classes :rewrite)

Theorem: ocst-block-conc-of-tree-fix-cst

(defthm ocst-block-conc-of-tree-fix-cst
  (equal (ocst-block-conc (abnf::tree-fix abnf::cst))
         (ocst-block-conc abnf::cst)))

Theorem: ocst-block-conc-tree-equiv-congruence-on-cst

(defthm ocst-block-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-block-conc abnf::cst)
                  (ocst-block-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc1

(defun ocst-statement-conc1 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    1))))
 (let ((__function__ 'ocst-statement-conc1))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc1

(defthm tree-list-listp-of-ocst-statement-conc1
  (b* ((abnf::cstss (ocst-statement-conc1 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc1-match

(defthm ocst-statement-conc1-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       1))
           (b* ((abnf::cstss (ocst-statement-conc1 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "block")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc1-of-tree-fix-cst

(defthm ocst-statement-conc1-of-tree-fix-cst
  (equal (ocst-statement-conc1 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc1 abnf::cst)))

Theorem: ocst-statement-conc1-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc1-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc1 abnf::cst)
                  (ocst-statement-conc1 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc2

(defun ocst-statement-conc2 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    2))))
 (let ((__function__ 'ocst-statement-conc2))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc2

(defthm tree-list-listp-of-ocst-statement-conc2
  (b* ((abnf::cstss (ocst-statement-conc2 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc2-match

(defthm ocst-statement-conc2-match
 (implies
   (and (ocst-matchp abnf::cst "statement")
        (equal (ocst-statement-conc? abnf::cst)
               2))
   (b* ((abnf::cstss (ocst-statement-conc2 abnf::cst)))
     (ocst-list-list-conc-matchp abnf::cstss "functiondefinition")))
 :rule-classes :rewrite)

Theorem: ocst-statement-conc2-of-tree-fix-cst

(defthm ocst-statement-conc2-of-tree-fix-cst
  (equal (ocst-statement-conc2 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc2 abnf::cst)))

Theorem: ocst-statement-conc2-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc2-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc2 abnf::cst)
                  (ocst-statement-conc2 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc3

(defun ocst-statement-conc3 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    3))))
 (let ((__function__ 'ocst-statement-conc3))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc3

(defthm tree-list-listp-of-ocst-statement-conc3
  (b* ((abnf::cstss (ocst-statement-conc3 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc3-match

(defthm ocst-statement-conc3-match
 (implies
  (and (ocst-matchp abnf::cst "statement")
       (equal (ocst-statement-conc? abnf::cst)
              3))
  (b* ((abnf::cstss (ocst-statement-conc3 abnf::cst)))
    (ocst-list-list-conc-matchp abnf::cstss "variabledeclaration")))
 :rule-classes :rewrite)

Theorem: ocst-statement-conc3-of-tree-fix-cst

(defthm ocst-statement-conc3-of-tree-fix-cst
  (equal (ocst-statement-conc3 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc3 abnf::cst)))

Theorem: ocst-statement-conc3-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc3-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc3 abnf::cst)
                  (ocst-statement-conc3 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc4

(defun ocst-statement-conc4 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    4))))
 (let ((__function__ 'ocst-statement-conc4))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc4

(defthm tree-list-listp-of-ocst-statement-conc4
  (b* ((abnf::cstss (ocst-statement-conc4 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc4-match

(defthm ocst-statement-conc4-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       4))
           (b* ((abnf::cstss (ocst-statement-conc4 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "assignment")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc4-of-tree-fix-cst

(defthm ocst-statement-conc4-of-tree-fix-cst
  (equal (ocst-statement-conc4 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc4 abnf::cst)))

Theorem: ocst-statement-conc4-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc4-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc4 abnf::cst)
                  (ocst-statement-conc4 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc5

(defun ocst-statement-conc5 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    5))))
 (let ((__function__ 'ocst-statement-conc5))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc5

(defthm tree-list-listp-of-ocst-statement-conc5
  (b* ((abnf::cstss (ocst-statement-conc5 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc5-match

(defthm ocst-statement-conc5-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       5))
           (b* ((abnf::cstss (ocst-statement-conc5 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "if")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc5-of-tree-fix-cst

(defthm ocst-statement-conc5-of-tree-fix-cst
  (equal (ocst-statement-conc5 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc5 abnf::cst)))

Theorem: ocst-statement-conc5-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc5-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc5 abnf::cst)
                  (ocst-statement-conc5 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc6

(defun ocst-statement-conc6 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    6))))
 (let ((__function__ 'ocst-statement-conc6))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc6

(defthm tree-list-listp-of-ocst-statement-conc6
  (b* ((abnf::cstss (ocst-statement-conc6 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc6-match

(defthm ocst-statement-conc6-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       6))
           (b* ((abnf::cstss (ocst-statement-conc6 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "expression")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc6-of-tree-fix-cst

(defthm ocst-statement-conc6-of-tree-fix-cst
  (equal (ocst-statement-conc6 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc6 abnf::cst)))

Theorem: ocst-statement-conc6-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc6-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc6 abnf::cst)
                  (ocst-statement-conc6 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc7

(defun ocst-statement-conc7 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    7))))
 (let ((__function__ 'ocst-statement-conc7))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc7

(defthm tree-list-listp-of-ocst-statement-conc7
  (b* ((abnf::cstss (ocst-statement-conc7 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc7-match

(defthm ocst-statement-conc7-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       7))
           (b* ((abnf::cstss (ocst-statement-conc7 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "switch")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc7-of-tree-fix-cst

(defthm ocst-statement-conc7-of-tree-fix-cst
  (equal (ocst-statement-conc7 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc7 abnf::cst)))

Theorem: ocst-statement-conc7-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc7-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc7 abnf::cst)
                  (ocst-statement-conc7 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc8

(defun ocst-statement-conc8 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    8))))
 (let ((__function__ 'ocst-statement-conc8))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc8

(defthm tree-list-listp-of-ocst-statement-conc8
  (b* ((abnf::cstss (ocst-statement-conc8 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc8-match

(defthm ocst-statement-conc8-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       8))
           (b* ((abnf::cstss (ocst-statement-conc8 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "forloop")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc8-of-tree-fix-cst

(defthm ocst-statement-conc8-of-tree-fix-cst
  (equal (ocst-statement-conc8 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc8 abnf::cst)))

Theorem: ocst-statement-conc8-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc8-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc8 abnf::cst)
                  (ocst-statement-conc8 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc9

(defun ocst-statement-conc9 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    9))))
 (let ((__function__ 'ocst-statement-conc9))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc9

(defthm tree-list-listp-of-ocst-statement-conc9
  (b* ((abnf::cstss (ocst-statement-conc9 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc9-match

(defthm ocst-statement-conc9-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   9))
       (b* ((abnf::cstss (ocst-statement-conc9 abnf::cst)))
         (ocst-list-list-conc-matchp abnf::cstss "breakcontinue")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc9-of-tree-fix-cst

(defthm ocst-statement-conc9-of-tree-fix-cst
  (equal (ocst-statement-conc9 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc9 abnf::cst)))

Theorem: ocst-statement-conc9-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc9-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc9 abnf::cst)
                  (ocst-statement-conc9 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc10

(defun ocst-statement-conc10 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    10))))
 (let ((__function__ 'ocst-statement-conc10))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-statement-conc10

(defthm tree-list-listp-of-ocst-statement-conc10
  (b* ((abnf::cstss (ocst-statement-conc10 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc10-match

(defthm ocst-statement-conc10-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       10))
           (b* ((abnf::cstss (ocst-statement-conc10 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "leave")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc10-of-tree-fix-cst

(defthm ocst-statement-conc10-of-tree-fix-cst
  (equal (ocst-statement-conc10 (abnf::tree-fix abnf::cst))
         (ocst-statement-conc10 abnf::cst)))

Theorem: ocst-statement-conc10-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc10-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc10 abnf::cst)
                  (ocst-statement-conc10 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-functiondefinition-conc

(defun ocst-functiondefinition-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (ocst-matchp abnf::cst "functiondefinition")))
  (let ((__function__ 'ocst-functiondefinition-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-functiondefinition-conc

(defthm tree-list-listp-of-ocst-functiondefinition-conc
  (b* ((abnf::cstss (ocst-functiondefinition-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-functiondefinition-conc-match

(defthm ocst-functiondefinition-conc-match
 (implies
  (ocst-matchp abnf::cst "functiondefinition")
  (b* ((abnf::cstss (ocst-functiondefinition-conc abnf::cst)))
   (ocst-list-list-conc-matchp
    abnf::cstss
    "%s\"function\" identifier \"(\" [ typedidentifierlist ] \")\" [ \"->\" typedidentifierlist ] block")))
 :rule-classes :rewrite)

Theorem: ocst-functiondefinition-conc-of-tree-fix-cst

(defthm ocst-functiondefinition-conc-of-tree-fix-cst
  (equal (ocst-functiondefinition-conc (abnf::tree-fix abnf::cst))
         (ocst-functiondefinition-conc abnf::cst)))

Theorem: ocst-functiondefinition-conc-tree-equiv-congruence-on-cst

(defthm ocst-functiondefinition-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-functiondefinition-conc abnf::cst)
                  (ocst-functiondefinition-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-variabledeclaration-conc

(defun ocst-variabledeclaration-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (ocst-matchp abnf::cst "variabledeclaration")))
  (let ((__function__ 'ocst-variabledeclaration-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-variabledeclaration-conc

(defthm tree-list-listp-of-ocst-variabledeclaration-conc
  (b* ((abnf::cstss (ocst-variabledeclaration-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-variabledeclaration-conc-match

(defthm ocst-variabledeclaration-conc-match
  (implies
       (ocst-matchp abnf::cst "variabledeclaration")
       (b* ((abnf::cstss (ocst-variabledeclaration-conc abnf::cst)))
         (ocst-list-list-conc-matchp
              abnf::cstss
              "%s\"let\" typedidentifierlist [ \":=\" expression ]")))
  :rule-classes :rewrite)

Theorem: ocst-variabledeclaration-conc-of-tree-fix-cst

(defthm ocst-variabledeclaration-conc-of-tree-fix-cst
  (equal (ocst-variabledeclaration-conc (abnf::tree-fix abnf::cst))
         (ocst-variabledeclaration-conc abnf::cst)))

Theorem: ocst-variabledeclaration-conc-tree-equiv-congruence-on-cst

(defthm ocst-variabledeclaration-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-variabledeclaration-conc abnf::cst)
                  (ocst-variabledeclaration-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-assignment-conc

(defun ocst-assignment-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "assignment")))
  (let ((__function__ 'ocst-assignment-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-assignment-conc

(defthm tree-list-listp-of-ocst-assignment-conc
  (b* ((abnf::cstss (ocst-assignment-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-assignment-conc-match

(defthm ocst-assignment-conc-match
 (implies
   (ocst-matchp abnf::cst "assignment")
   (b* ((abnf::cstss (ocst-assignment-conc abnf::cst)))
     (ocst-list-list-conc-matchp abnf::cstss
                                 "identifierlist \":=\" expression")))
 :rule-classes :rewrite)

Theorem: ocst-assignment-conc-of-tree-fix-cst

(defthm ocst-assignment-conc-of-tree-fix-cst
  (equal (ocst-assignment-conc (abnf::tree-fix abnf::cst))
         (ocst-assignment-conc abnf::cst)))

Theorem: ocst-assignment-conc-tree-equiv-congruence-on-cst

(defthm ocst-assignment-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-assignment-conc abnf::cst)
                  (ocst-assignment-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc1

(defun ocst-expression-conc1 (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (ocst-matchp abnf::cst "expression")
                          (equal (ocst-expression-conc? abnf::cst)
                                 1))))
  (let ((__function__ 'ocst-expression-conc1))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-expression-conc1

(defthm tree-list-listp-of-ocst-expression-conc1
  (b* ((abnf::cstss (ocst-expression-conc1 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc1-match

(defthm ocst-expression-conc1-match
  (implies
       (and (ocst-matchp abnf::cst "expression")
            (equal (ocst-expression-conc? abnf::cst)
                   1))
       (b* ((abnf::cstss (ocst-expression-conc1 abnf::cst)))
         (ocst-list-list-conc-matchp abnf::cstss "functioncall")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc1-of-tree-fix-cst

(defthm ocst-expression-conc1-of-tree-fix-cst
  (equal (ocst-expression-conc1 (abnf::tree-fix abnf::cst))
         (ocst-expression-conc1 abnf::cst)))

Theorem: ocst-expression-conc1-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc1-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc1 abnf::cst)
                  (ocst-expression-conc1 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc2

(defun ocst-expression-conc2 (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (ocst-matchp abnf::cst "expression")
                          (equal (ocst-expression-conc? abnf::cst)
                                 2))))
  (let ((__function__ 'ocst-expression-conc2))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-expression-conc2

(defthm tree-list-listp-of-ocst-expression-conc2
  (b* ((abnf::cstss (ocst-expression-conc2 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc2-match

(defthm ocst-expression-conc2-match
  (implies (and (ocst-matchp abnf::cst "expression")
                (equal (ocst-expression-conc? abnf::cst)
                       2))
           (b* ((abnf::cstss (ocst-expression-conc2 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "identifier")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc2-of-tree-fix-cst

(defthm ocst-expression-conc2-of-tree-fix-cst
  (equal (ocst-expression-conc2 (abnf::tree-fix abnf::cst))
         (ocst-expression-conc2 abnf::cst)))

Theorem: ocst-expression-conc2-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc2-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc2 abnf::cst)
                  (ocst-expression-conc2 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc3

(defun ocst-expression-conc3 (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (ocst-matchp abnf::cst "expression")
                          (equal (ocst-expression-conc? abnf::cst)
                                 3))))
  (let ((__function__ 'ocst-expression-conc3))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-expression-conc3

(defthm tree-list-listp-of-ocst-expression-conc3
  (b* ((abnf::cstss (ocst-expression-conc3 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc3-match

(defthm ocst-expression-conc3-match
  (implies (and (ocst-matchp abnf::cst "expression")
                (equal (ocst-expression-conc? abnf::cst)
                       3))
           (b* ((abnf::cstss (ocst-expression-conc3 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "literal")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc3-of-tree-fix-cst

(defthm ocst-expression-conc3-of-tree-fix-cst
  (equal (ocst-expression-conc3 (abnf::tree-fix abnf::cst))
         (ocst-expression-conc3 abnf::cst)))

Theorem: ocst-expression-conc3-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc3-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc3 abnf::cst)
                  (ocst-expression-conc3 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-if-conc

(defun ocst-if-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "if")))
  (let ((__function__ 'ocst-if-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-if-conc

(defthm tree-list-listp-of-ocst-if-conc
  (b* ((abnf::cstss (ocst-if-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-if-conc-match

(defthm ocst-if-conc-match
  (implies (ocst-matchp abnf::cst "if")
           (b* ((abnf::cstss (ocst-if-conc abnf::cst)))
             (ocst-list-list-conc-matchp
                  abnf::cstss "%s\"if\" expression block")))
  :rule-classes :rewrite)

Theorem: ocst-if-conc-of-tree-fix-cst

(defthm ocst-if-conc-of-tree-fix-cst
  (equal (ocst-if-conc (abnf::tree-fix abnf::cst))
         (ocst-if-conc abnf::cst)))

Theorem: ocst-if-conc-tree-equiv-congruence-on-cst

(defthm ocst-if-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-if-conc abnf::cst)
                  (ocst-if-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-switch-conc

(defun ocst-switch-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "switch")))
  (let ((__function__ 'ocst-switch-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-switch-conc

(defthm tree-list-listp-of-ocst-switch-conc
  (b* ((abnf::cstss (ocst-switch-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-switch-conc-match

(defthm ocst-switch-conc-match
 (implies
  (ocst-matchp abnf::cst "switch")
  (b* ((abnf::cstss (ocst-switch-conc abnf::cst)))
    (ocst-list-list-conc-matchp
         abnf::cstss
         "%s\"switch\" expression ( 1*case [ default ] / default )")))
 :rule-classes :rewrite)

Theorem: ocst-switch-conc-of-tree-fix-cst

(defthm ocst-switch-conc-of-tree-fix-cst
  (equal (ocst-switch-conc (abnf::tree-fix abnf::cst))
         (ocst-switch-conc abnf::cst)))

Theorem: ocst-switch-conc-tree-equiv-congruence-on-cst

(defthm ocst-switch-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-switch-conc abnf::cst)
                  (ocst-switch-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-case-conc

(defun ocst-case-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "case")))
  (let ((__function__ 'ocst-case-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-case-conc

(defthm tree-list-listp-of-ocst-case-conc
  (b* ((abnf::cstss (ocst-case-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-case-conc-match

(defthm ocst-case-conc-match
  (implies (ocst-matchp abnf::cst "case")
           (b* ((abnf::cstss (ocst-case-conc abnf::cst)))
             (ocst-list-list-conc-matchp
                  abnf::cstss "%s\"case\" literal block")))
  :rule-classes :rewrite)

Theorem: ocst-case-conc-of-tree-fix-cst

(defthm ocst-case-conc-of-tree-fix-cst
  (equal (ocst-case-conc (abnf::tree-fix abnf::cst))
         (ocst-case-conc abnf::cst)))

Theorem: ocst-case-conc-tree-equiv-congruence-on-cst

(defthm ocst-case-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-case-conc abnf::cst)
                  (ocst-case-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-default-conc

(defun ocst-default-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "default")))
  (let ((__function__ 'ocst-default-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-default-conc

(defthm tree-list-listp-of-ocst-default-conc
  (b* ((abnf::cstss (ocst-default-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-default-conc-match

(defthm ocst-default-conc-match
 (implies
    (ocst-matchp abnf::cst "default")
    (b* ((abnf::cstss (ocst-default-conc abnf::cst)))
      (ocst-list-list-conc-matchp abnf::cstss "%s\"default\" block")))
 :rule-classes :rewrite)

Theorem: ocst-default-conc-of-tree-fix-cst

(defthm ocst-default-conc-of-tree-fix-cst
  (equal (ocst-default-conc (abnf::tree-fix abnf::cst))
         (ocst-default-conc abnf::cst)))

Theorem: ocst-default-conc-tree-equiv-congruence-on-cst

(defthm ocst-default-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-default-conc abnf::cst)
                  (ocst-default-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-forloop-conc

(defun ocst-forloop-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "forloop")))
  (let ((__function__ 'ocst-forloop-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-forloop-conc

(defthm tree-list-listp-of-ocst-forloop-conc
  (b* ((abnf::cstss (ocst-forloop-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-forloop-conc-match

(defthm ocst-forloop-conc-match
  (implies (ocst-matchp abnf::cst "forloop")
           (b* ((abnf::cstss (ocst-forloop-conc abnf::cst)))
             (ocst-list-list-conc-matchp
                  abnf::cstss
                  "%s\"for\" block expression block block")))
  :rule-classes :rewrite)

Theorem: ocst-forloop-conc-of-tree-fix-cst

(defthm ocst-forloop-conc-of-tree-fix-cst
  (equal (ocst-forloop-conc (abnf::tree-fix abnf::cst))
         (ocst-forloop-conc abnf::cst)))

Theorem: ocst-forloop-conc-tree-equiv-congruence-on-cst

(defthm ocst-forloop-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-forloop-conc abnf::cst)
                  (ocst-forloop-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-leave-conc

(defun ocst-leave-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "leave")))
  (let ((__function__ 'ocst-leave-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-leave-conc

(defthm tree-list-listp-of-ocst-leave-conc
  (b* ((abnf::cstss (ocst-leave-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-leave-conc-match

(defthm ocst-leave-conc-match
  (implies (ocst-matchp abnf::cst "leave")
           (b* ((abnf::cstss (ocst-leave-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%s\"leave\"")))
  :rule-classes :rewrite)

Theorem: ocst-leave-conc-of-tree-fix-cst

(defthm ocst-leave-conc-of-tree-fix-cst
  (equal (ocst-leave-conc (abnf::tree-fix abnf::cst))
         (ocst-leave-conc abnf::cst)))

Theorem: ocst-leave-conc-tree-equiv-congruence-on-cst

(defthm ocst-leave-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-leave-conc abnf::cst)
                  (ocst-leave-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-functioncall-conc

(defun ocst-functioncall-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "functioncall")))
  (let ((__function__ 'ocst-functioncall-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-functioncall-conc

(defthm tree-list-listp-of-ocst-functioncall-conc
  (b* ((abnf::cstss (ocst-functioncall-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-functioncall-conc-match

(defthm ocst-functioncall-conc-match
 (implies
   (ocst-matchp abnf::cst "functioncall")
   (b* ((abnf::cstss (ocst-functioncall-conc abnf::cst)))
     (ocst-list-list-conc-matchp
          abnf::cstss
          "identifier \"(\" [ expression *( \",\" expression ) ] \")\"")))
 :rule-classes :rewrite)

Theorem: ocst-functioncall-conc-of-tree-fix-cst

(defthm ocst-functioncall-conc-of-tree-fix-cst
  (equal (ocst-functioncall-conc (abnf::tree-fix abnf::cst))
         (ocst-functioncall-conc abnf::cst)))

Theorem: ocst-functioncall-conc-tree-equiv-congruence-on-cst

(defthm ocst-functioncall-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-functioncall-conc abnf::cst)
                  (ocst-functioncall-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-lowercaseletter-conc

(defun ocst-lowercaseletter-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "lowercaseletter")))
  (let ((__function__ 'ocst-lowercaseletter-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-lowercaseletter-conc

(defthm tree-list-listp-of-ocst-lowercaseletter-conc
  (b* ((abnf::cstss (ocst-lowercaseletter-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-lowercaseletter-conc-match

(defthm ocst-lowercaseletter-conc-match
  (implies (ocst-matchp abnf::cst "lowercaseletter")
           (b* ((abnf::cstss (ocst-lowercaseletter-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%x61-7A")))
  :rule-classes :rewrite)

Theorem: ocst-lowercaseletter-conc-of-tree-fix-cst

(defthm ocst-lowercaseletter-conc-of-tree-fix-cst
  (equal (ocst-lowercaseletter-conc (abnf::tree-fix abnf::cst))
         (ocst-lowercaseletter-conc abnf::cst)))

Theorem: ocst-lowercaseletter-conc-tree-equiv-congruence-on-cst

(defthm ocst-lowercaseletter-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-lowercaseletter-conc abnf::cst)
                  (ocst-lowercaseletter-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-uppercaseletter-conc

(defun ocst-uppercaseletter-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "uppercaseletter")))
  (let ((__function__ 'ocst-uppercaseletter-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-uppercaseletter-conc

(defthm tree-list-listp-of-ocst-uppercaseletter-conc
  (b* ((abnf::cstss (ocst-uppercaseletter-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-uppercaseletter-conc-match

(defthm ocst-uppercaseletter-conc-match
  (implies (ocst-matchp abnf::cst "uppercaseletter")
           (b* ((abnf::cstss (ocst-uppercaseletter-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%x41-5A")))
  :rule-classes :rewrite)

Theorem: ocst-uppercaseletter-conc-of-tree-fix-cst

(defthm ocst-uppercaseletter-conc-of-tree-fix-cst
  (equal (ocst-uppercaseletter-conc (abnf::tree-fix abnf::cst))
         (ocst-uppercaseletter-conc abnf::cst)))

Theorem: ocst-uppercaseletter-conc-tree-equiv-congruence-on-cst

(defthm ocst-uppercaseletter-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-uppercaseletter-conc abnf::cst)
                  (ocst-uppercaseletter-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-identifier-conc

(defun ocst-identifier-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "identifier")))
  (let ((__function__ 'ocst-identifier-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-identifier-conc

(defthm tree-list-listp-of-ocst-identifier-conc
  (b* ((abnf::cstss (ocst-identifier-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-identifier-conc-match

(defthm ocst-identifier-conc-match
 (implies
  (ocst-matchp abnf::cst "identifier")
  (b* ((abnf::cstss (ocst-identifier-conc abnf::cst)))
    (ocst-list-list-conc-matchp abnf::cstss
                                "identifierstart *identifierrest")))
 :rule-classes :rewrite)

Theorem: ocst-identifier-conc-of-tree-fix-cst

(defthm ocst-identifier-conc-of-tree-fix-cst
  (equal (ocst-identifier-conc (abnf::tree-fix abnf::cst))
         (ocst-identifier-conc abnf::cst)))

Theorem: ocst-identifier-conc-tree-equiv-congruence-on-cst

(defthm ocst-identifier-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-identifier-conc abnf::cst)
                  (ocst-identifier-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-identifierlist-conc

(defun ocst-identifierlist-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "identifierlist")))
  (let ((__function__ 'ocst-identifierlist-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-identifierlist-conc

(defthm tree-list-listp-of-ocst-identifierlist-conc
  (b* ((abnf::cstss (ocst-identifierlist-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-identifierlist-conc-match

(defthm ocst-identifierlist-conc-match
 (implies
   (ocst-matchp abnf::cst "identifierlist")
   (b* ((abnf::cstss (ocst-identifierlist-conc abnf::cst)))
     (ocst-list-list-conc-matchp abnf::cstss
                                 "identifier *( \",\" identifier )")))
 :rule-classes :rewrite)

Theorem: ocst-identifierlist-conc-of-tree-fix-cst

(defthm ocst-identifierlist-conc-of-tree-fix-cst
  (equal (ocst-identifierlist-conc (abnf::tree-fix abnf::cst))
         (ocst-identifierlist-conc abnf::cst)))

Theorem: ocst-identifierlist-conc-tree-equiv-congruence-on-cst

(defthm ocst-identifierlist-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-identifierlist-conc abnf::cst)
                  (ocst-identifierlist-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-typename-conc

(defun ocst-typename-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "typename")))
  (let ((__function__ 'ocst-typename-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-typename-conc

(defthm tree-list-listp-of-ocst-typename-conc
  (b* ((abnf::cstss (ocst-typename-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-typename-conc-match

(defthm ocst-typename-conc-match
  (implies (ocst-matchp abnf::cst "typename")
           (b* ((abnf::cstss (ocst-typename-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "identifier")))
  :rule-classes :rewrite)

Theorem: ocst-typename-conc-of-tree-fix-cst

(defthm ocst-typename-conc-of-tree-fix-cst
  (equal (ocst-typename-conc (abnf::tree-fix abnf::cst))
         (ocst-typename-conc abnf::cst)))

Theorem: ocst-typename-conc-tree-equiv-congruence-on-cst

(defthm ocst-typename-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-typename-conc abnf::cst)
                  (ocst-typename-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-typedidentifierlist-conc

(defun ocst-typedidentifierlist-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (ocst-matchp abnf::cst "typedidentifierlist")))
  (let ((__function__ 'ocst-typedidentifierlist-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-typedidentifierlist-conc

(defthm tree-list-listp-of-ocst-typedidentifierlist-conc
  (b* ((abnf::cstss (ocst-typedidentifierlist-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-typedidentifierlist-conc-match

(defthm ocst-typedidentifierlist-conc-match
 (implies
  (ocst-matchp abnf::cst "typedidentifierlist")
  (b* ((abnf::cstss (ocst-typedidentifierlist-conc abnf::cst)))
   (ocst-list-list-conc-matchp
    abnf::cstss
    "identifier [ \":\" typename ] *( \",\" identifier [ \":\" typename ] )")))
 :rule-classes :rewrite)

Theorem: ocst-typedidentifierlist-conc-of-tree-fix-cst

(defthm ocst-typedidentifierlist-conc-of-tree-fix-cst
  (equal (ocst-typedidentifierlist-conc (abnf::tree-fix abnf::cst))
         (ocst-typedidentifierlist-conc abnf::cst)))

Theorem: ocst-typedidentifierlist-conc-tree-equiv-congruence-on-cst

(defthm ocst-typedidentifierlist-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-typedidentifierlist-conc abnf::cst)
                  (ocst-typedidentifierlist-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-literal-conc

(defun ocst-literal-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "literal")))
  (let ((__function__ 'ocst-literal-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-literal-conc

(defthm tree-list-listp-of-ocst-literal-conc
  (b* ((abnf::cstss (ocst-literal-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-literal-conc-match

(defthm ocst-literal-conc-match
 (implies
  (ocst-matchp abnf::cst "literal")
  (b* ((abnf::cstss (ocst-literal-conc abnf::cst)))
   (ocst-list-list-conc-matchp
    abnf::cstss
    "( numberliteral / stringliteral / trueliteral / falseliteral ) [ \":\" typename ]")))
 :rule-classes :rewrite)

Theorem: ocst-literal-conc-of-tree-fix-cst

(defthm ocst-literal-conc-of-tree-fix-cst
  (equal (ocst-literal-conc (abnf::tree-fix abnf::cst))
         (ocst-literal-conc abnf::cst)))

Theorem: ocst-literal-conc-tree-equiv-congruence-on-cst

(defthm ocst-literal-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-literal-conc abnf::cst)
                  (ocst-literal-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-numberliteral-conc1

(defun ocst-numberliteral-conc1 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "numberliteral")
                         (equal (ocst-numberliteral-conc? abnf::cst)
                                1))))
 (let ((__function__ 'ocst-numberliteral-conc1))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-numberliteral-conc1

(defthm tree-list-listp-of-ocst-numberliteral-conc1
  (b* ((abnf::cstss (ocst-numberliteral-conc1 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc1-match

(defthm ocst-numberliteral-conc1-match
  (implies (and (ocst-matchp abnf::cst "numberliteral")
                (equal (ocst-numberliteral-conc? abnf::cst)
                       1))
           (b* ((abnf::cstss (ocst-numberliteral-conc1 abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "hexnumber")))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc1-of-tree-fix-cst

(defthm ocst-numberliteral-conc1-of-tree-fix-cst
  (equal (ocst-numberliteral-conc1 (abnf::tree-fix abnf::cst))
         (ocst-numberliteral-conc1 abnf::cst)))

Theorem: ocst-numberliteral-conc1-tree-equiv-congruence-on-cst

(defthm ocst-numberliteral-conc1-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc1 abnf::cst)
                  (ocst-numberliteral-conc1 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-numberliteral-conc2

(defun ocst-numberliteral-conc2 (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "numberliteral")
                         (equal (ocst-numberliteral-conc? abnf::cst)
                                2))))
 (let ((__function__ 'ocst-numberliteral-conc2))
   (declare (ignorable __function__))
   (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-numberliteral-conc2

(defthm tree-list-listp-of-ocst-numberliteral-conc2
  (b* ((abnf::cstss (ocst-numberliteral-conc2 abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc2-match

(defthm ocst-numberliteral-conc2-match
  (implies
       (and (ocst-matchp abnf::cst "numberliteral")
            (equal (ocst-numberliteral-conc? abnf::cst)
                   2))
       (b* ((abnf::cstss (ocst-numberliteral-conc2 abnf::cst)))
         (ocst-list-list-conc-matchp abnf::cstss "decimalnumber")))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc2-of-tree-fix-cst

(defthm ocst-numberliteral-conc2-of-tree-fix-cst
  (equal (ocst-numberliteral-conc2 (abnf::tree-fix abnf::cst))
         (ocst-numberliteral-conc2 abnf::cst)))

Theorem: ocst-numberliteral-conc2-tree-equiv-congruence-on-cst

(defthm ocst-numberliteral-conc2-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc2 abnf::cst)
                  (ocst-numberliteral-conc2 cst-equiv)))
  :rule-classes :congruence)

Function: ocst-dquote-conc

(defun ocst-dquote-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "dquote")))
  (let ((__function__ 'ocst-dquote-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-dquote-conc

(defthm tree-list-listp-of-ocst-dquote-conc
  (b* ((abnf::cstss (ocst-dquote-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-dquote-conc-match

(defthm ocst-dquote-conc-match
  (implies (ocst-matchp abnf::cst "dquote")
           (b* ((abnf::cstss (ocst-dquote-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%x22")))
  :rule-classes :rewrite)

Theorem: ocst-dquote-conc-of-tree-fix-cst

(defthm ocst-dquote-conc-of-tree-fix-cst
  (equal (ocst-dquote-conc (abnf::tree-fix abnf::cst))
         (ocst-dquote-conc abnf::cst)))

Theorem: ocst-dquote-conc-tree-equiv-congruence-on-cst

(defthm ocst-dquote-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-dquote-conc abnf::cst)
                  (ocst-dquote-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-any-conc

(defun ocst-any-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "any")))
  (let ((__function__ 'ocst-any-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-any-conc

(defthm tree-list-listp-of-ocst-any-conc
  (b* ((abnf::cstss (ocst-any-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-any-conc-match

(defthm ocst-any-conc-match
  (implies (ocst-matchp abnf::cst "any")
           (b* ((abnf::cstss (ocst-any-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%x0-10FFFF")))
  :rule-classes :rewrite)

Theorem: ocst-any-conc-of-tree-fix-cst

(defthm ocst-any-conc-of-tree-fix-cst
  (equal (ocst-any-conc (abnf::tree-fix abnf::cst))
         (ocst-any-conc abnf::cst)))

Theorem: ocst-any-conc-tree-equiv-congruence-on-cst

(defthm ocst-any-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-any-conc abnf::cst)
                  (ocst-any-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-stringliteral-conc

(defun ocst-stringliteral-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "stringliteral")))
  (let ((__function__ 'ocst-stringliteral-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-stringliteral-conc

(defthm tree-list-listp-of-ocst-stringliteral-conc
  (b* ((abnf::cstss (ocst-stringliteral-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-stringliteral-conc-match

(defthm ocst-stringliteral-conc-match
  (implies (ocst-matchp abnf::cst "stringliteral")
           (b* ((abnf::cstss (ocst-stringliteral-conc abnf::cst)))
             (ocst-list-list-conc-matchp
                  abnf::cstss
                  "dquote *( not-dquote-cr-lf / \"\\\" any ) dquote")))
  :rule-classes :rewrite)

Theorem: ocst-stringliteral-conc-of-tree-fix-cst

(defthm ocst-stringliteral-conc-of-tree-fix-cst
  (equal (ocst-stringliteral-conc (abnf::tree-fix abnf::cst))
         (ocst-stringliteral-conc abnf::cst)))

Theorem: ocst-stringliteral-conc-tree-equiv-congruence-on-cst

(defthm ocst-stringliteral-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-stringliteral-conc abnf::cst)
                  (ocst-stringliteral-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-trueliteral-conc

(defun ocst-trueliteral-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "trueliteral")))
  (let ((__function__ 'ocst-trueliteral-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-trueliteral-conc

(defthm tree-list-listp-of-ocst-trueliteral-conc
  (b* ((abnf::cstss (ocst-trueliteral-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-trueliteral-conc-match

(defthm ocst-trueliteral-conc-match
  (implies (ocst-matchp abnf::cst "trueliteral")
           (b* ((abnf::cstss (ocst-trueliteral-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%s\"true\"")))
  :rule-classes :rewrite)

Theorem: ocst-trueliteral-conc-of-tree-fix-cst

(defthm ocst-trueliteral-conc-of-tree-fix-cst
  (equal (ocst-trueliteral-conc (abnf::tree-fix abnf::cst))
         (ocst-trueliteral-conc abnf::cst)))

Theorem: ocst-trueliteral-conc-tree-equiv-congruence-on-cst

(defthm ocst-trueliteral-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-trueliteral-conc abnf::cst)
                  (ocst-trueliteral-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-falseliteral-conc

(defun ocst-falseliteral-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "falseliteral")))
  (let ((__function__ 'ocst-falseliteral-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-falseliteral-conc

(defthm tree-list-listp-of-ocst-falseliteral-conc
  (b* ((abnf::cstss (ocst-falseliteral-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-falseliteral-conc-match

(defthm ocst-falseliteral-conc-match
  (implies (ocst-matchp abnf::cst "falseliteral")
           (b* ((abnf::cstss (ocst-falseliteral-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%s\"false\"")))
  :rule-classes :rewrite)

Theorem: ocst-falseliteral-conc-of-tree-fix-cst

(defthm ocst-falseliteral-conc-of-tree-fix-cst
  (equal (ocst-falseliteral-conc (abnf::tree-fix abnf::cst))
         (ocst-falseliteral-conc abnf::cst)))

Theorem: ocst-falseliteral-conc-tree-equiv-congruence-on-cst

(defthm ocst-falseliteral-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-falseliteral-conc abnf::cst)
                  (ocst-falseliteral-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-decimaldigit-conc

(defun ocst-decimaldigit-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "decimaldigit")))
  (let ((__function__ 'ocst-decimaldigit-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-decimaldigit-conc

(defthm tree-list-listp-of-ocst-decimaldigit-conc
  (b* ((abnf::cstss (ocst-decimaldigit-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-decimaldigit-conc-match

(defthm ocst-decimaldigit-conc-match
  (implies (ocst-matchp abnf::cst "decimaldigit")
           (b* ((abnf::cstss (ocst-decimaldigit-conc abnf::cst)))
             (ocst-list-list-conc-matchp abnf::cstss "%x30-39")))
  :rule-classes :rewrite)

Theorem: ocst-decimaldigit-conc-of-tree-fix-cst

(defthm ocst-decimaldigit-conc-of-tree-fix-cst
  (equal (ocst-decimaldigit-conc (abnf::tree-fix abnf::cst))
         (ocst-decimaldigit-conc abnf::cst)))

Theorem: ocst-decimaldigit-conc-tree-equiv-congruence-on-cst

(defthm ocst-decimaldigit-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-decimaldigit-conc abnf::cst)
                  (ocst-decimaldigit-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-hexnumber-conc

(defun ocst-hexnumber-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "hexnumber")))
  (let ((__function__ 'ocst-hexnumber-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-hexnumber-conc

(defthm tree-list-listp-of-ocst-hexnumber-conc
  (b* ((abnf::cstss (ocst-hexnumber-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-hexnumber-conc-match

(defthm ocst-hexnumber-conc-match
 (implies
    (ocst-matchp abnf::cst "hexnumber")
    (b* ((abnf::cstss (ocst-hexnumber-conc abnf::cst)))
      (ocst-list-list-conc-matchp abnf::cstss "%s\"0x\" 1*hexdigit")))
 :rule-classes :rewrite)

Theorem: ocst-hexnumber-conc-of-tree-fix-cst

(defthm ocst-hexnumber-conc-of-tree-fix-cst
  (equal (ocst-hexnumber-conc (abnf::tree-fix abnf::cst))
         (ocst-hexnumber-conc abnf::cst)))

Theorem: ocst-hexnumber-conc-tree-equiv-congruence-on-cst

(defthm ocst-hexnumber-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-hexnumber-conc abnf::cst)
                  (ocst-hexnumber-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-decimalnumber-conc

(defun ocst-decimalnumber-conc (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "decimalnumber")))
  (let ((__function__ 'ocst-decimalnumber-conc))
    (declare (ignorable __function__))
    (abnf::tree-nonleaf->branches abnf::cst)))

Theorem: tree-list-listp-of-ocst-decimalnumber-conc

(defthm tree-list-listp-of-ocst-decimalnumber-conc
  (b* ((abnf::cstss (ocst-decimalnumber-conc abnf::cst)))
    (abnf::tree-list-listp abnf::cstss))
  :rule-classes :rewrite)

Theorem: ocst-decimalnumber-conc-match

(defthm ocst-decimalnumber-conc-match
  (implies
       (ocst-matchp abnf::cst "decimalnumber")
       (b* ((abnf::cstss (ocst-decimalnumber-conc abnf::cst)))
         (ocst-list-list-conc-matchp abnf::cstss "1*decimaldigit")))
  :rule-classes :rewrite)

Theorem: ocst-decimalnumber-conc-of-tree-fix-cst

(defthm ocst-decimalnumber-conc-of-tree-fix-cst
  (equal (ocst-decimalnumber-conc (abnf::tree-fix abnf::cst))
         (ocst-decimalnumber-conc abnf::cst)))

Theorem: ocst-decimalnumber-conc-tree-equiv-congruence-on-cst

(defthm ocst-decimalnumber-conc-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-decimalnumber-conc abnf::cst)
                  (ocst-decimalnumber-conc cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc1-rep

(defun ocst-statement-conc1-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    1))))
 (let ((__function__ 'ocst-statement-conc1-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc1 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc1-rep

(defthm tree-listp-of-ocst-statement-conc1-rep
  (b* ((abnf::csts (ocst-statement-conc1-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc1-rep-match

(defthm ocst-statement-conc1-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       1))
           (b* ((abnf::csts (ocst-statement-conc1-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "block")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc1-rep-of-tree-fix-cst

(defthm ocst-statement-conc1-rep-of-tree-fix-cst
  (equal (ocst-statement-conc1-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc1-rep abnf::cst)))

Theorem: ocst-statement-conc1-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc1-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc1-rep abnf::cst)
                  (ocst-statement-conc1-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc2-rep

(defun ocst-statement-conc2-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    2))))
 (let ((__function__ 'ocst-statement-conc2-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc2 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc2-rep

(defthm tree-listp-of-ocst-statement-conc2-rep
  (b* ((abnf::csts (ocst-statement-conc2-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc2-rep-match

(defthm ocst-statement-conc2-rep-match
 (implies (and (ocst-matchp abnf::cst "statement")
               (equal (ocst-statement-conc? abnf::cst)
                      2))
          (b* ((abnf::csts (ocst-statement-conc2-rep abnf::cst)))
            (ocst-list-rep-matchp abnf::csts "functiondefinition")))
 :rule-classes :rewrite)

Theorem: ocst-statement-conc2-rep-of-tree-fix-cst

(defthm ocst-statement-conc2-rep-of-tree-fix-cst
  (equal (ocst-statement-conc2-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc2-rep abnf::cst)))

Theorem: ocst-statement-conc2-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc2-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc2-rep abnf::cst)
                  (ocst-statement-conc2-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc3-rep

(defun ocst-statement-conc3-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    3))))
 (let ((__function__ 'ocst-statement-conc3-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc3 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc3-rep

(defthm tree-listp-of-ocst-statement-conc3-rep
  (b* ((abnf::csts (ocst-statement-conc3-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc3-rep-match

(defthm ocst-statement-conc3-rep-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   3))
       (b* ((abnf::csts (ocst-statement-conc3-rep abnf::cst)))
         (ocst-list-rep-matchp abnf::csts "variabledeclaration")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc3-rep-of-tree-fix-cst

(defthm ocst-statement-conc3-rep-of-tree-fix-cst
  (equal (ocst-statement-conc3-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc3-rep abnf::cst)))

Theorem: ocst-statement-conc3-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc3-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc3-rep abnf::cst)
                  (ocst-statement-conc3-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc4-rep

(defun ocst-statement-conc4-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    4))))
 (let ((__function__ 'ocst-statement-conc4-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc4 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc4-rep

(defthm tree-listp-of-ocst-statement-conc4-rep
  (b* ((abnf::csts (ocst-statement-conc4-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc4-rep-match

(defthm ocst-statement-conc4-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       4))
           (b* ((abnf::csts (ocst-statement-conc4-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "assignment")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc4-rep-of-tree-fix-cst

(defthm ocst-statement-conc4-rep-of-tree-fix-cst
  (equal (ocst-statement-conc4-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc4-rep abnf::cst)))

Theorem: ocst-statement-conc4-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc4-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc4-rep abnf::cst)
                  (ocst-statement-conc4-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc5-rep

(defun ocst-statement-conc5-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    5))))
 (let ((__function__ 'ocst-statement-conc5-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc5 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc5-rep

(defthm tree-listp-of-ocst-statement-conc5-rep
  (b* ((abnf::csts (ocst-statement-conc5-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc5-rep-match

(defthm ocst-statement-conc5-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       5))
           (b* ((abnf::csts (ocst-statement-conc5-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "if")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc5-rep-of-tree-fix-cst

(defthm ocst-statement-conc5-rep-of-tree-fix-cst
  (equal (ocst-statement-conc5-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc5-rep abnf::cst)))

Theorem: ocst-statement-conc5-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc5-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc5-rep abnf::cst)
                  (ocst-statement-conc5-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc6-rep

(defun ocst-statement-conc6-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    6))))
 (let ((__function__ 'ocst-statement-conc6-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc6 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc6-rep

(defthm tree-listp-of-ocst-statement-conc6-rep
  (b* ((abnf::csts (ocst-statement-conc6-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc6-rep-match

(defthm ocst-statement-conc6-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       6))
           (b* ((abnf::csts (ocst-statement-conc6-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "expression")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc6-rep-of-tree-fix-cst

(defthm ocst-statement-conc6-rep-of-tree-fix-cst
  (equal (ocst-statement-conc6-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc6-rep abnf::cst)))

Theorem: ocst-statement-conc6-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc6-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc6-rep abnf::cst)
                  (ocst-statement-conc6-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc7-rep

(defun ocst-statement-conc7-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    7))))
 (let ((__function__ 'ocst-statement-conc7-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc7 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc7-rep

(defthm tree-listp-of-ocst-statement-conc7-rep
  (b* ((abnf::csts (ocst-statement-conc7-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc7-rep-match

(defthm ocst-statement-conc7-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       7))
           (b* ((abnf::csts (ocst-statement-conc7-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "switch")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc7-rep-of-tree-fix-cst

(defthm ocst-statement-conc7-rep-of-tree-fix-cst
  (equal (ocst-statement-conc7-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc7-rep abnf::cst)))

Theorem: ocst-statement-conc7-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc7-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc7-rep abnf::cst)
                  (ocst-statement-conc7-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc8-rep

(defun ocst-statement-conc8-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    8))))
 (let ((__function__ 'ocst-statement-conc8-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc8 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc8-rep

(defthm tree-listp-of-ocst-statement-conc8-rep
  (b* ((abnf::csts (ocst-statement-conc8-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc8-rep-match

(defthm ocst-statement-conc8-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       8))
           (b* ((abnf::csts (ocst-statement-conc8-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "forloop")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc8-rep-of-tree-fix-cst

(defthm ocst-statement-conc8-rep-of-tree-fix-cst
  (equal (ocst-statement-conc8-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc8-rep abnf::cst)))

Theorem: ocst-statement-conc8-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc8-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc8-rep abnf::cst)
                  (ocst-statement-conc8-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc9-rep

(defun ocst-statement-conc9-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    9))))
 (let ((__function__ 'ocst-statement-conc9-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc9 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc9-rep

(defthm tree-listp-of-ocst-statement-conc9-rep
  (b* ((abnf::csts (ocst-statement-conc9-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc9-rep-match

(defthm ocst-statement-conc9-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       9))
           (b* ((abnf::csts (ocst-statement-conc9-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "breakcontinue")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc9-rep-of-tree-fix-cst

(defthm ocst-statement-conc9-rep-of-tree-fix-cst
  (equal (ocst-statement-conc9-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc9-rep abnf::cst)))

Theorem: ocst-statement-conc9-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc9-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc9-rep abnf::cst)
                  (ocst-statement-conc9-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc10-rep

(defun ocst-statement-conc10-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    10))))
 (let ((__function__ 'ocst-statement-conc10-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-statement-conc10 abnf::cst)))))

Theorem: tree-listp-of-ocst-statement-conc10-rep

(defthm tree-listp-of-ocst-statement-conc10-rep
  (b* ((abnf::csts (ocst-statement-conc10-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc10-rep-match

(defthm ocst-statement-conc10-rep-match
  (implies (and (ocst-matchp abnf::cst "statement")
                (equal (ocst-statement-conc? abnf::cst)
                       10))
           (b* ((abnf::csts (ocst-statement-conc10-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "leave")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc10-rep-of-tree-fix-cst

(defthm ocst-statement-conc10-rep-of-tree-fix-cst
  (equal (ocst-statement-conc10-rep (abnf::tree-fix abnf::cst))
         (ocst-statement-conc10-rep abnf::cst)))

Theorem: ocst-statement-conc10-rep-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc10-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc10-rep abnf::cst)
                  (ocst-statement-conc10-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc1-rep

(defun ocst-expression-conc1-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "expression")
                         (equal (ocst-expression-conc? abnf::cst)
                                1))))
 (let ((__function__ 'ocst-expression-conc1-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-expression-conc1 abnf::cst)))))

Theorem: tree-listp-of-ocst-expression-conc1-rep

(defthm tree-listp-of-ocst-expression-conc1-rep
  (b* ((abnf::csts (ocst-expression-conc1-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc1-rep-match

(defthm ocst-expression-conc1-rep-match
  (implies (and (ocst-matchp abnf::cst "expression")
                (equal (ocst-expression-conc? abnf::cst)
                       1))
           (b* ((abnf::csts (ocst-expression-conc1-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "functioncall")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc1-rep-of-tree-fix-cst

(defthm ocst-expression-conc1-rep-of-tree-fix-cst
  (equal (ocst-expression-conc1-rep (abnf::tree-fix abnf::cst))
         (ocst-expression-conc1-rep abnf::cst)))

Theorem: ocst-expression-conc1-rep-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc1-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc1-rep abnf::cst)
                  (ocst-expression-conc1-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc2-rep

(defun ocst-expression-conc2-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "expression")
                         (equal (ocst-expression-conc? abnf::cst)
                                2))))
 (let ((__function__ 'ocst-expression-conc2-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-expression-conc2 abnf::cst)))))

Theorem: tree-listp-of-ocst-expression-conc2-rep

(defthm tree-listp-of-ocst-expression-conc2-rep
  (b* ((abnf::csts (ocst-expression-conc2-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc2-rep-match

(defthm ocst-expression-conc2-rep-match
  (implies (and (ocst-matchp abnf::cst "expression")
                (equal (ocst-expression-conc? abnf::cst)
                       2))
           (b* ((abnf::csts (ocst-expression-conc2-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "identifier")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc2-rep-of-tree-fix-cst

(defthm ocst-expression-conc2-rep-of-tree-fix-cst
  (equal (ocst-expression-conc2-rep (abnf::tree-fix abnf::cst))
         (ocst-expression-conc2-rep abnf::cst)))

Theorem: ocst-expression-conc2-rep-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc2-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc2-rep abnf::cst)
                  (ocst-expression-conc2-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc3-rep

(defun ocst-expression-conc3-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "expression")
                         (equal (ocst-expression-conc? abnf::cst)
                                3))))
 (let ((__function__ 'ocst-expression-conc3-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-expression-conc3 abnf::cst)))))

Theorem: tree-listp-of-ocst-expression-conc3-rep

(defthm tree-listp-of-ocst-expression-conc3-rep
  (b* ((abnf::csts (ocst-expression-conc3-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc3-rep-match

(defthm ocst-expression-conc3-rep-match
  (implies (and (ocst-matchp abnf::cst "expression")
                (equal (ocst-expression-conc? abnf::cst)
                       3))
           (b* ((abnf::csts (ocst-expression-conc3-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "literal")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc3-rep-of-tree-fix-cst

(defthm ocst-expression-conc3-rep-of-tree-fix-cst
  (equal (ocst-expression-conc3-rep (abnf::tree-fix abnf::cst))
         (ocst-expression-conc3-rep abnf::cst)))

Theorem: ocst-expression-conc3-rep-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc3-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc3-rep abnf::cst)
                  (ocst-expression-conc3-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-leave-conc-rep

(defun ocst-leave-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "leave")))
  (let ((__function__ 'ocst-leave-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (ocst-leave-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-leave-conc-rep

(defthm tree-listp-of-ocst-leave-conc-rep
  (b* ((abnf::csts (ocst-leave-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-leave-conc-rep-match

(defthm ocst-leave-conc-rep-match
  (implies (ocst-matchp abnf::cst "leave")
           (b* ((abnf::csts (ocst-leave-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "%s\"leave\"")))
  :rule-classes :rewrite)

Theorem: ocst-leave-conc-rep-of-tree-fix-cst

(defthm ocst-leave-conc-rep-of-tree-fix-cst
  (equal (ocst-leave-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-leave-conc-rep abnf::cst)))

Theorem: ocst-leave-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-leave-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-leave-conc-rep abnf::cst)
                  (ocst-leave-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-lowercaseletter-conc-rep

(defun ocst-lowercaseletter-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "lowercaseletter")))
  (let ((__function__ 'ocst-lowercaseletter-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix
         (nth 0
              (ocst-lowercaseletter-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-lowercaseletter-conc-rep

(defthm tree-listp-of-ocst-lowercaseletter-conc-rep
  (b* ((abnf::csts (ocst-lowercaseletter-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-lowercaseletter-conc-rep-match

(defthm ocst-lowercaseletter-conc-rep-match
  (implies
       (ocst-matchp abnf::cst "lowercaseletter")
       (b* ((abnf::csts (ocst-lowercaseletter-conc-rep abnf::cst)))
         (ocst-list-rep-matchp abnf::csts "%x61-7A")))
  :rule-classes :rewrite)

Theorem: ocst-lowercaseletter-conc-rep-of-tree-fix-cst

(defthm ocst-lowercaseletter-conc-rep-of-tree-fix-cst
  (equal (ocst-lowercaseletter-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-lowercaseletter-conc-rep abnf::cst)))

Theorem: ocst-lowercaseletter-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-lowercaseletter-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-lowercaseletter-conc-rep abnf::cst)
                  (ocst-lowercaseletter-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-uppercaseletter-conc-rep

(defun ocst-uppercaseletter-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "uppercaseletter")))
  (let ((__function__ 'ocst-uppercaseletter-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix
         (nth 0
              (ocst-uppercaseletter-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-uppercaseletter-conc-rep

(defthm tree-listp-of-ocst-uppercaseletter-conc-rep
  (b* ((abnf::csts (ocst-uppercaseletter-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-uppercaseletter-conc-rep-match

(defthm ocst-uppercaseletter-conc-rep-match
  (implies
       (ocst-matchp abnf::cst "uppercaseletter")
       (b* ((abnf::csts (ocst-uppercaseletter-conc-rep abnf::cst)))
         (ocst-list-rep-matchp abnf::csts "%x41-5A")))
  :rule-classes :rewrite)

Theorem: ocst-uppercaseletter-conc-rep-of-tree-fix-cst

(defthm ocst-uppercaseletter-conc-rep-of-tree-fix-cst
  (equal (ocst-uppercaseletter-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-uppercaseletter-conc-rep abnf::cst)))

Theorem: ocst-uppercaseletter-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-uppercaseletter-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-uppercaseletter-conc-rep abnf::cst)
                  (ocst-uppercaseletter-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-typename-conc-rep

(defun ocst-typename-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "typename")))
  (let ((__function__ 'ocst-typename-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (ocst-typename-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-typename-conc-rep

(defthm tree-listp-of-ocst-typename-conc-rep
  (b* ((abnf::csts (ocst-typename-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-typename-conc-rep-match

(defthm ocst-typename-conc-rep-match
  (implies (ocst-matchp abnf::cst "typename")
           (b* ((abnf::csts (ocst-typename-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "identifier")))
  :rule-classes :rewrite)

Theorem: ocst-typename-conc-rep-of-tree-fix-cst

(defthm ocst-typename-conc-rep-of-tree-fix-cst
  (equal (ocst-typename-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-typename-conc-rep abnf::cst)))

Theorem: ocst-typename-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-typename-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-typename-conc-rep abnf::cst)
                  (ocst-typename-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-numberliteral-conc1-rep

(defun ocst-numberliteral-conc1-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "numberliteral")
                         (equal (ocst-numberliteral-conc? abnf::cst)
                                1))))
 (let ((__function__ 'ocst-numberliteral-conc1-rep))
  (declare (ignorable __function__))
  (abnf::tree-list-fix (nth 0
                            (ocst-numberliteral-conc1 abnf::cst)))))

Theorem: tree-listp-of-ocst-numberliteral-conc1-rep

(defthm tree-listp-of-ocst-numberliteral-conc1-rep
  (b* ((abnf::csts (ocst-numberliteral-conc1-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc1-rep-match

(defthm ocst-numberliteral-conc1-rep-match
  (implies
       (and (ocst-matchp abnf::cst "numberliteral")
            (equal (ocst-numberliteral-conc? abnf::cst)
                   1))
       (b* ((abnf::csts (ocst-numberliteral-conc1-rep abnf::cst)))
         (ocst-list-rep-matchp abnf::csts "hexnumber")))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc1-rep-of-tree-fix-cst

(defthm ocst-numberliteral-conc1-rep-of-tree-fix-cst
  (equal (ocst-numberliteral-conc1-rep (abnf::tree-fix abnf::cst))
         (ocst-numberliteral-conc1-rep abnf::cst)))

Theorem: ocst-numberliteral-conc1-rep-tree-equiv-congruence-on-cst

(defthm ocst-numberliteral-conc1-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc1-rep abnf::cst)
                  (ocst-numberliteral-conc1-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-numberliteral-conc2-rep

(defun ocst-numberliteral-conc2-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "numberliteral")
                         (equal (ocst-numberliteral-conc? abnf::cst)
                                2))))
 (let ((__function__ 'ocst-numberliteral-conc2-rep))
  (declare (ignorable __function__))
  (abnf::tree-list-fix (nth 0
                            (ocst-numberliteral-conc2 abnf::cst)))))

Theorem: tree-listp-of-ocst-numberliteral-conc2-rep

(defthm tree-listp-of-ocst-numberliteral-conc2-rep
  (b* ((abnf::csts (ocst-numberliteral-conc2-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc2-rep-match

(defthm ocst-numberliteral-conc2-rep-match
  (implies
       (and (ocst-matchp abnf::cst "numberliteral")
            (equal (ocst-numberliteral-conc? abnf::cst)
                   2))
       (b* ((abnf::csts (ocst-numberliteral-conc2-rep abnf::cst)))
         (ocst-list-rep-matchp abnf::csts "decimalnumber")))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc2-rep-of-tree-fix-cst

(defthm ocst-numberliteral-conc2-rep-of-tree-fix-cst
  (equal (ocst-numberliteral-conc2-rep (abnf::tree-fix abnf::cst))
         (ocst-numberliteral-conc2-rep abnf::cst)))

Theorem: ocst-numberliteral-conc2-rep-tree-equiv-congruence-on-cst

(defthm ocst-numberliteral-conc2-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc2-rep abnf::cst)
                  (ocst-numberliteral-conc2-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-dquote-conc-rep

(defun ocst-dquote-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "dquote")))
  (let ((__function__ 'ocst-dquote-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (ocst-dquote-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-dquote-conc-rep

(defthm tree-listp-of-ocst-dquote-conc-rep
  (b* ((abnf::csts (ocst-dquote-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-dquote-conc-rep-match

(defthm ocst-dquote-conc-rep-match
  (implies (ocst-matchp abnf::cst "dquote")
           (b* ((abnf::csts (ocst-dquote-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "%x22")))
  :rule-classes :rewrite)

Theorem: ocst-dquote-conc-rep-of-tree-fix-cst

(defthm ocst-dquote-conc-rep-of-tree-fix-cst
  (equal (ocst-dquote-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-dquote-conc-rep abnf::cst)))

Theorem: ocst-dquote-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-dquote-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-dquote-conc-rep abnf::cst)
                  (ocst-dquote-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-any-conc-rep

(defun ocst-any-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "any")))
  (let ((__function__ 'ocst-any-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (ocst-any-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-any-conc-rep

(defthm tree-listp-of-ocst-any-conc-rep
  (b* ((abnf::csts (ocst-any-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-any-conc-rep-match

(defthm ocst-any-conc-rep-match
  (implies (ocst-matchp abnf::cst "any")
           (b* ((abnf::csts (ocst-any-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "%x0-10FFFF")))
  :rule-classes :rewrite)

Theorem: ocst-any-conc-rep-of-tree-fix-cst

(defthm ocst-any-conc-rep-of-tree-fix-cst
  (equal (ocst-any-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-any-conc-rep abnf::cst)))

Theorem: ocst-any-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-any-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-any-conc-rep abnf::cst)
                  (ocst-any-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-trueliteral-conc-rep

(defun ocst-trueliteral-conc-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "trueliteral")))
 (let ((__function__ 'ocst-trueliteral-conc-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0 (ocst-trueliteral-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-trueliteral-conc-rep

(defthm tree-listp-of-ocst-trueliteral-conc-rep
  (b* ((abnf::csts (ocst-trueliteral-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-trueliteral-conc-rep-match

(defthm ocst-trueliteral-conc-rep-match
  (implies (ocst-matchp abnf::cst "trueliteral")
           (b* ((abnf::csts (ocst-trueliteral-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "%s\"true\"")))
  :rule-classes :rewrite)

Theorem: ocst-trueliteral-conc-rep-of-tree-fix-cst

(defthm ocst-trueliteral-conc-rep-of-tree-fix-cst
  (equal (ocst-trueliteral-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-trueliteral-conc-rep abnf::cst)))

Theorem: ocst-trueliteral-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-trueliteral-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-trueliteral-conc-rep abnf::cst)
                  (ocst-trueliteral-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-falseliteral-conc-rep

(defun ocst-falseliteral-conc-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "falseliteral")))
 (let ((__function__ 'ocst-falseliteral-conc-rep))
  (declare (ignorable __function__))
  (abnf::tree-list-fix (nth 0 (ocst-falseliteral-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-falseliteral-conc-rep

(defthm tree-listp-of-ocst-falseliteral-conc-rep
  (b* ((abnf::csts (ocst-falseliteral-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-falseliteral-conc-rep-match

(defthm ocst-falseliteral-conc-rep-match
  (implies (ocst-matchp abnf::cst "falseliteral")
           (b* ((abnf::csts (ocst-falseliteral-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "%s\"false\"")))
  :rule-classes :rewrite)

Theorem: ocst-falseliteral-conc-rep-of-tree-fix-cst

(defthm ocst-falseliteral-conc-rep-of-tree-fix-cst
  (equal (ocst-falseliteral-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-falseliteral-conc-rep abnf::cst)))

Theorem: ocst-falseliteral-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-falseliteral-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-falseliteral-conc-rep abnf::cst)
                  (ocst-falseliteral-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-decimaldigit-conc-rep

(defun ocst-decimaldigit-conc-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "decimaldigit")))
 (let ((__function__ 'ocst-decimaldigit-conc-rep))
  (declare (ignorable __function__))
  (abnf::tree-list-fix (nth 0 (ocst-decimaldigit-conc abnf::cst)))))

Theorem: tree-listp-of-ocst-decimaldigit-conc-rep

(defthm tree-listp-of-ocst-decimaldigit-conc-rep
  (b* ((abnf::csts (ocst-decimaldigit-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: ocst-decimaldigit-conc-rep-match

(defthm ocst-decimaldigit-conc-rep-match
  (implies (ocst-matchp abnf::cst "decimaldigit")
           (b* ((abnf::csts (ocst-decimaldigit-conc-rep abnf::cst)))
             (ocst-list-rep-matchp abnf::csts "%x30-39")))
  :rule-classes :rewrite)

Theorem: ocst-decimaldigit-conc-rep-of-tree-fix-cst

(defthm ocst-decimaldigit-conc-rep-of-tree-fix-cst
  (equal (ocst-decimaldigit-conc-rep (abnf::tree-fix abnf::cst))
         (ocst-decimaldigit-conc-rep abnf::cst)))

Theorem: ocst-decimaldigit-conc-rep-tree-equiv-congruence-on-cst

(defthm ocst-decimaldigit-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-decimaldigit-conc-rep abnf::cst)
                  (ocst-decimaldigit-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc1-rep-elem

(defun ocst-statement-conc1-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    1))))
 (let ((__function__ 'ocst-statement-conc1-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc1-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc1-rep-elem

(defthm treep-of-ocst-statement-conc1-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc1-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc1-rep-elem-match

(defthm ocst-statement-conc1-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   1))
       (b* ((abnf::cst1 (ocst-statement-conc1-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "block")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc1-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc1-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc1-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc1-rep-elem abnf::cst)))

Theorem: ocst-statement-conc1-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc1-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc1-rep-elem abnf::cst)
                  (ocst-statement-conc1-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc2-rep-elem

(defun ocst-statement-conc2-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    2))))
 (let ((__function__ 'ocst-statement-conc2-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc2-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc2-rep-elem

(defthm treep-of-ocst-statement-conc2-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc2-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc2-rep-elem-match

(defthm ocst-statement-conc2-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   2))
       (b* ((abnf::cst1 (ocst-statement-conc2-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "functiondefinition")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc2-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc2-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc2-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc2-rep-elem abnf::cst)))

Theorem: ocst-statement-conc2-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc2-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc2-rep-elem abnf::cst)
                  (ocst-statement-conc2-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc3-rep-elem

(defun ocst-statement-conc3-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    3))))
 (let ((__function__ 'ocst-statement-conc3-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc3-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc3-rep-elem

(defthm treep-of-ocst-statement-conc3-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc3-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc3-rep-elem-match

(defthm ocst-statement-conc3-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   3))
       (b* ((abnf::cst1 (ocst-statement-conc3-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "variabledeclaration")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc3-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc3-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc3-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc3-rep-elem abnf::cst)))

Theorem: ocst-statement-conc3-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc3-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc3-rep-elem abnf::cst)
                  (ocst-statement-conc3-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc4-rep-elem

(defun ocst-statement-conc4-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    4))))
 (let ((__function__ 'ocst-statement-conc4-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc4-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc4-rep-elem

(defthm treep-of-ocst-statement-conc4-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc4-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc4-rep-elem-match

(defthm ocst-statement-conc4-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   4))
       (b* ((abnf::cst1 (ocst-statement-conc4-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "assignment")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc4-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc4-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc4-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc4-rep-elem abnf::cst)))

Theorem: ocst-statement-conc4-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc4-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc4-rep-elem abnf::cst)
                  (ocst-statement-conc4-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc5-rep-elem

(defun ocst-statement-conc5-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    5))))
 (let ((__function__ 'ocst-statement-conc5-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc5-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc5-rep-elem

(defthm treep-of-ocst-statement-conc5-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc5-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc5-rep-elem-match

(defthm ocst-statement-conc5-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   5))
       (b* ((abnf::cst1 (ocst-statement-conc5-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "if")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc5-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc5-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc5-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc5-rep-elem abnf::cst)))

Theorem: ocst-statement-conc5-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc5-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc5-rep-elem abnf::cst)
                  (ocst-statement-conc5-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc6-rep-elem

(defun ocst-statement-conc6-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    6))))
 (let ((__function__ 'ocst-statement-conc6-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc6-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc6-rep-elem

(defthm treep-of-ocst-statement-conc6-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc6-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc6-rep-elem-match

(defthm ocst-statement-conc6-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   6))
       (b* ((abnf::cst1 (ocst-statement-conc6-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "expression")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc6-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc6-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc6-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc6-rep-elem abnf::cst)))

Theorem: ocst-statement-conc6-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc6-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc6-rep-elem abnf::cst)
                  (ocst-statement-conc6-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc7-rep-elem

(defun ocst-statement-conc7-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    7))))
 (let ((__function__ 'ocst-statement-conc7-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc7-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc7-rep-elem

(defthm treep-of-ocst-statement-conc7-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc7-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc7-rep-elem-match

(defthm ocst-statement-conc7-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   7))
       (b* ((abnf::cst1 (ocst-statement-conc7-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "switch")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc7-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc7-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc7-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc7-rep-elem abnf::cst)))

Theorem: ocst-statement-conc7-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc7-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc7-rep-elem abnf::cst)
                  (ocst-statement-conc7-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc8-rep-elem

(defun ocst-statement-conc8-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    8))))
 (let ((__function__ 'ocst-statement-conc8-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc8-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc8-rep-elem

(defthm treep-of-ocst-statement-conc8-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc8-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc8-rep-elem-match

(defthm ocst-statement-conc8-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   8))
       (b* ((abnf::cst1 (ocst-statement-conc8-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "forloop")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc8-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc8-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc8-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc8-rep-elem abnf::cst)))

Theorem: ocst-statement-conc8-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc8-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc8-rep-elem abnf::cst)
                  (ocst-statement-conc8-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc9-rep-elem

(defun ocst-statement-conc9-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    9))))
 (let ((__function__ 'ocst-statement-conc9-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc9-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc9-rep-elem

(defthm treep-of-ocst-statement-conc9-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc9-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc9-rep-elem-match

(defthm ocst-statement-conc9-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   9))
       (b* ((abnf::cst1 (ocst-statement-conc9-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "breakcontinue")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc9-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc9-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc9-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc9-rep-elem abnf::cst)))

Theorem: ocst-statement-conc9-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc9-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc9-rep-elem abnf::cst)
                  (ocst-statement-conc9-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-statement-conc10-rep-elem

(defun ocst-statement-conc10-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (and (ocst-matchp abnf::cst "statement")
                             (equal (ocst-statement-conc? abnf::cst)
                                    10))))
 (let ((__function__ 'ocst-statement-conc10-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-statement-conc10-rep abnf::cst)))))

Theorem: treep-of-ocst-statement-conc10-rep-elem

(defthm treep-of-ocst-statement-conc10-rep-elem
  (b* ((abnf::cst1 (ocst-statement-conc10-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc10-rep-elem-match

(defthm ocst-statement-conc10-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "statement")
            (equal (ocst-statement-conc? abnf::cst)
                   10))
       (b* ((abnf::cst1 (ocst-statement-conc10-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "leave")))
  :rule-classes :rewrite)

Theorem: ocst-statement-conc10-rep-elem-of-tree-fix-cst

(defthm ocst-statement-conc10-rep-elem-of-tree-fix-cst
  (equal (ocst-statement-conc10-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-statement-conc10-rep-elem abnf::cst)))

Theorem: ocst-statement-conc10-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-statement-conc10-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-statement-conc10-rep-elem abnf::cst)
                  (ocst-statement-conc10-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc1-rep-elem

(defun ocst-expression-conc1-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (ocst-matchp abnf::cst "expression")
                          (equal (ocst-expression-conc? abnf::cst)
                                 1))))
  (let ((__function__ 'ocst-expression-conc1-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (ocst-expression-conc1-rep abnf::cst)))))

Theorem: treep-of-ocst-expression-conc1-rep-elem

(defthm treep-of-ocst-expression-conc1-rep-elem
  (b* ((abnf::cst1 (ocst-expression-conc1-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc1-rep-elem-match

(defthm ocst-expression-conc1-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "expression")
            (equal (ocst-expression-conc? abnf::cst)
                   1))
       (b* ((abnf::cst1 (ocst-expression-conc1-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "functioncall")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc1-rep-elem-of-tree-fix-cst

(defthm ocst-expression-conc1-rep-elem-of-tree-fix-cst
  (equal (ocst-expression-conc1-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-expression-conc1-rep-elem abnf::cst)))

Theorem: ocst-expression-conc1-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc1-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc1-rep-elem abnf::cst)
                  (ocst-expression-conc1-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc2-rep-elem

(defun ocst-expression-conc2-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (ocst-matchp abnf::cst "expression")
                          (equal (ocst-expression-conc? abnf::cst)
                                 2))))
  (let ((__function__ 'ocst-expression-conc2-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (ocst-expression-conc2-rep abnf::cst)))))

Theorem: treep-of-ocst-expression-conc2-rep-elem

(defthm treep-of-ocst-expression-conc2-rep-elem
  (b* ((abnf::cst1 (ocst-expression-conc2-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc2-rep-elem-match

(defthm ocst-expression-conc2-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "expression")
            (equal (ocst-expression-conc? abnf::cst)
                   2))
       (b* ((abnf::cst1 (ocst-expression-conc2-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "identifier")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc2-rep-elem-of-tree-fix-cst

(defthm ocst-expression-conc2-rep-elem-of-tree-fix-cst
  (equal (ocst-expression-conc2-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-expression-conc2-rep-elem abnf::cst)))

Theorem: ocst-expression-conc2-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc2-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc2-rep-elem abnf::cst)
                  (ocst-expression-conc2-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-expression-conc3-rep-elem

(defun ocst-expression-conc3-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (ocst-matchp abnf::cst "expression")
                          (equal (ocst-expression-conc? abnf::cst)
                                 3))))
  (let ((__function__ 'ocst-expression-conc3-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (ocst-expression-conc3-rep abnf::cst)))))

Theorem: treep-of-ocst-expression-conc3-rep-elem

(defthm treep-of-ocst-expression-conc3-rep-elem
  (b* ((abnf::cst1 (ocst-expression-conc3-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc3-rep-elem-match

(defthm ocst-expression-conc3-rep-elem-match
  (implies
       (and (ocst-matchp abnf::cst "expression")
            (equal (ocst-expression-conc? abnf::cst)
                   3))
       (b* ((abnf::cst1 (ocst-expression-conc3-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "literal")))
  :rule-classes :rewrite)

Theorem: ocst-expression-conc3-rep-elem-of-tree-fix-cst

(defthm ocst-expression-conc3-rep-elem-of-tree-fix-cst
  (equal (ocst-expression-conc3-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-expression-conc3-rep-elem abnf::cst)))

Theorem: ocst-expression-conc3-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-expression-conc3-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-expression-conc3-rep-elem abnf::cst)
                  (ocst-expression-conc3-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-leave-conc-rep-elem

(defun ocst-leave-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "leave")))
  (let ((__function__ 'ocst-leave-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (ocst-leave-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-leave-conc-rep-elem

(defthm treep-of-ocst-leave-conc-rep-elem
  (b* ((abnf::cst1 (ocst-leave-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-leave-conc-rep-elem-match

(defthm ocst-leave-conc-rep-elem-match
  (implies (ocst-matchp abnf::cst "leave")
           (b* ((abnf::cst1 (ocst-leave-conc-rep-elem abnf::cst)))
             (ocst-matchp abnf::cst1 "%s\"leave\"")))
  :rule-classes :rewrite)

Theorem: ocst-leave-conc-rep-elem-of-tree-fix-cst

(defthm ocst-leave-conc-rep-elem-of-tree-fix-cst
  (equal (ocst-leave-conc-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-leave-conc-rep-elem abnf::cst)))

Theorem: ocst-leave-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-leave-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-leave-conc-rep-elem abnf::cst)
                  (ocst-leave-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-lowercaseletter-conc-rep-elem

(defun ocst-lowercaseletter-conc-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "lowercaseletter")))
 (let ((__function__ 'ocst-lowercaseletter-conc-rep-elem))
  (declare (ignorable __function__))
  (abnf::tree-fix (nth 0
                       (ocst-lowercaseletter-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-lowercaseletter-conc-rep-elem

(defthm treep-of-ocst-lowercaseletter-conc-rep-elem
  (b* ((abnf::cst1 (ocst-lowercaseletter-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-lowercaseletter-conc-rep-elem-match

(defthm ocst-lowercaseletter-conc-rep-elem-match
 (implies
   (ocst-matchp abnf::cst "lowercaseletter")
   (b* ((abnf::cst1 (ocst-lowercaseletter-conc-rep-elem abnf::cst)))
     (ocst-matchp abnf::cst1 "%x61-7A")))
 :rule-classes :rewrite)

Theorem: ocst-lowercaseletter-conc-rep-elem-of-tree-fix-cst

(defthm ocst-lowercaseletter-conc-rep-elem-of-tree-fix-cst
 (equal
     (ocst-lowercaseletter-conc-rep-elem (abnf::tree-fix abnf::cst))
     (ocst-lowercaseletter-conc-rep-elem abnf::cst)))

Theorem: ocst-lowercaseletter-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm
    ocst-lowercaseletter-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-lowercaseletter-conc-rep-elem abnf::cst)
                  (ocst-lowercaseletter-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-uppercaseletter-conc-rep-elem

(defun ocst-uppercaseletter-conc-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (ocst-matchp abnf::cst "uppercaseletter")))
 (let ((__function__ 'ocst-uppercaseletter-conc-rep-elem))
  (declare (ignorable __function__))
  (abnf::tree-fix (nth 0
                       (ocst-uppercaseletter-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-uppercaseletter-conc-rep-elem

(defthm treep-of-ocst-uppercaseletter-conc-rep-elem
  (b* ((abnf::cst1 (ocst-uppercaseletter-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-uppercaseletter-conc-rep-elem-match

(defthm ocst-uppercaseletter-conc-rep-elem-match
 (implies
   (ocst-matchp abnf::cst "uppercaseletter")
   (b* ((abnf::cst1 (ocst-uppercaseletter-conc-rep-elem abnf::cst)))
     (ocst-matchp abnf::cst1 "%x41-5A")))
 :rule-classes :rewrite)

Theorem: ocst-uppercaseletter-conc-rep-elem-of-tree-fix-cst

(defthm ocst-uppercaseletter-conc-rep-elem-of-tree-fix-cst
 (equal
     (ocst-uppercaseletter-conc-rep-elem (abnf::tree-fix abnf::cst))
     (ocst-uppercaseletter-conc-rep-elem abnf::cst)))

Theorem: ocst-uppercaseletter-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm
    ocst-uppercaseletter-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-uppercaseletter-conc-rep-elem abnf::cst)
                  (ocst-uppercaseletter-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-typename-conc-rep-elem

(defun ocst-typename-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "typename")))
  (let ((__function__ 'ocst-typename-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (ocst-typename-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-typename-conc-rep-elem

(defthm treep-of-ocst-typename-conc-rep-elem
  (b* ((abnf::cst1 (ocst-typename-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-typename-conc-rep-elem-match

(defthm ocst-typename-conc-rep-elem-match
 (implies (ocst-matchp abnf::cst "typename")
          (b* ((abnf::cst1 (ocst-typename-conc-rep-elem abnf::cst)))
            (ocst-matchp abnf::cst1 "identifier")))
 :rule-classes :rewrite)

Theorem: ocst-typename-conc-rep-elem-of-tree-fix-cst

(defthm ocst-typename-conc-rep-elem-of-tree-fix-cst
  (equal (ocst-typename-conc-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-typename-conc-rep-elem abnf::cst)))

Theorem: ocst-typename-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-typename-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-typename-conc-rep-elem abnf::cst)
                  (ocst-typename-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-numberliteral-conc1-rep-elem

(defun ocst-numberliteral-conc1-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "numberliteral")
                         (equal (ocst-numberliteral-conc? abnf::cst)
                                1))))
 (let ((__function__ 'ocst-numberliteral-conc1-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-numberliteral-conc1-rep abnf::cst)))))

Theorem: treep-of-ocst-numberliteral-conc1-rep-elem

(defthm treep-of-ocst-numberliteral-conc1-rep-elem
  (b* ((abnf::cst1 (ocst-numberliteral-conc1-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc1-rep-elem-match

(defthm ocst-numberliteral-conc1-rep-elem-match
 (implies
    (and (ocst-matchp abnf::cst "numberliteral")
         (equal (ocst-numberliteral-conc? abnf::cst)
                1))
    (b* ((abnf::cst1 (ocst-numberliteral-conc1-rep-elem abnf::cst)))
      (ocst-matchp abnf::cst1 "hexnumber")))
 :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc1-rep-elem-of-tree-fix-cst

(defthm ocst-numberliteral-conc1-rep-elem-of-tree-fix-cst
 (equal
      (ocst-numberliteral-conc1-rep-elem (abnf::tree-fix abnf::cst))
      (ocst-numberliteral-conc1-rep-elem abnf::cst)))

Theorem: ocst-numberliteral-conc1-rep-elem-tree-equiv-congruence-on-cst

(defthm
     ocst-numberliteral-conc1-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc1-rep-elem abnf::cst)
                  (ocst-numberliteral-conc1-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-numberliteral-conc2-rep-elem

(defun ocst-numberliteral-conc2-rep-elem (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare
      (xargs :guard (and (ocst-matchp abnf::cst "numberliteral")
                         (equal (ocst-numberliteral-conc? abnf::cst)
                                2))))
 (let ((__function__ 'ocst-numberliteral-conc2-rep-elem))
   (declare (ignorable __function__))
   (abnf::tree-fix (nth 0
                        (ocst-numberliteral-conc2-rep abnf::cst)))))

Theorem: treep-of-ocst-numberliteral-conc2-rep-elem

(defthm treep-of-ocst-numberliteral-conc2-rep-elem
  (b* ((abnf::cst1 (ocst-numberliteral-conc2-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc2-rep-elem-match

(defthm ocst-numberliteral-conc2-rep-elem-match
 (implies
    (and (ocst-matchp abnf::cst "numberliteral")
         (equal (ocst-numberliteral-conc? abnf::cst)
                2))
    (b* ((abnf::cst1 (ocst-numberliteral-conc2-rep-elem abnf::cst)))
      (ocst-matchp abnf::cst1 "decimalnumber")))
 :rule-classes :rewrite)

Theorem: ocst-numberliteral-conc2-rep-elem-of-tree-fix-cst

(defthm ocst-numberliteral-conc2-rep-elem-of-tree-fix-cst
 (equal
      (ocst-numberliteral-conc2-rep-elem (abnf::tree-fix abnf::cst))
      (ocst-numberliteral-conc2-rep-elem abnf::cst)))

Theorem: ocst-numberliteral-conc2-rep-elem-tree-equiv-congruence-on-cst

(defthm
     ocst-numberliteral-conc2-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-numberliteral-conc2-rep-elem abnf::cst)
                  (ocst-numberliteral-conc2-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-dquote-conc-rep-elem

(defun ocst-dquote-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "dquote")))
  (let ((__function__ 'ocst-dquote-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (ocst-dquote-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-dquote-conc-rep-elem

(defthm treep-of-ocst-dquote-conc-rep-elem
  (b* ((abnf::cst1 (ocst-dquote-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-dquote-conc-rep-elem-match

(defthm ocst-dquote-conc-rep-elem-match
  (implies (ocst-matchp abnf::cst "dquote")
           (b* ((abnf::cst1 (ocst-dquote-conc-rep-elem abnf::cst)))
             (ocst-matchp abnf::cst1 "%x22")))
  :rule-classes :rewrite)

Theorem: ocst-dquote-conc-rep-elem-of-tree-fix-cst

(defthm ocst-dquote-conc-rep-elem-of-tree-fix-cst
  (equal (ocst-dquote-conc-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-dquote-conc-rep-elem abnf::cst)))

Theorem: ocst-dquote-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-dquote-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-dquote-conc-rep-elem abnf::cst)
                  (ocst-dquote-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-any-conc-rep-elem

(defun ocst-any-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "any")))
  (let ((__function__ 'ocst-any-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (ocst-any-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-any-conc-rep-elem

(defthm treep-of-ocst-any-conc-rep-elem
  (b* ((abnf::cst1 (ocst-any-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-any-conc-rep-elem-match

(defthm ocst-any-conc-rep-elem-match
  (implies (ocst-matchp abnf::cst "any")
           (b* ((abnf::cst1 (ocst-any-conc-rep-elem abnf::cst)))
             (ocst-matchp abnf::cst1 "%x0-10FFFF")))
  :rule-classes :rewrite)

Theorem: ocst-any-conc-rep-elem-of-tree-fix-cst

(defthm ocst-any-conc-rep-elem-of-tree-fix-cst
  (equal (ocst-any-conc-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-any-conc-rep-elem abnf::cst)))

Theorem: ocst-any-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-any-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-any-conc-rep-elem abnf::cst)
                  (ocst-any-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-trueliteral-conc-rep-elem

(defun ocst-trueliteral-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "trueliteral")))
  (let ((__function__ 'ocst-trueliteral-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (ocst-trueliteral-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-trueliteral-conc-rep-elem

(defthm treep-of-ocst-trueliteral-conc-rep-elem
  (b* ((abnf::cst1 (ocst-trueliteral-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-trueliteral-conc-rep-elem-match

(defthm ocst-trueliteral-conc-rep-elem-match
  (implies
       (ocst-matchp abnf::cst "trueliteral")
       (b* ((abnf::cst1 (ocst-trueliteral-conc-rep-elem abnf::cst)))
         (ocst-matchp abnf::cst1 "%s\"true\"")))
  :rule-classes :rewrite)

Theorem: ocst-trueliteral-conc-rep-elem-of-tree-fix-cst

(defthm ocst-trueliteral-conc-rep-elem-of-tree-fix-cst
  (equal (ocst-trueliteral-conc-rep-elem (abnf::tree-fix abnf::cst))
         (ocst-trueliteral-conc-rep-elem abnf::cst)))

Theorem: ocst-trueliteral-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-trueliteral-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-trueliteral-conc-rep-elem abnf::cst)
                  (ocst-trueliteral-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-falseliteral-conc-rep-elem

(defun ocst-falseliteral-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "falseliteral")))
  (let ((__function__ 'ocst-falseliteral-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (ocst-falseliteral-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-falseliteral-conc-rep-elem

(defthm treep-of-ocst-falseliteral-conc-rep-elem
  (b* ((abnf::cst1 (ocst-falseliteral-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-falseliteral-conc-rep-elem-match

(defthm ocst-falseliteral-conc-rep-elem-match
 (implies
      (ocst-matchp abnf::cst "falseliteral")
      (b* ((abnf::cst1 (ocst-falseliteral-conc-rep-elem abnf::cst)))
        (ocst-matchp abnf::cst1 "%s\"false\"")))
 :rule-classes :rewrite)

Theorem: ocst-falseliteral-conc-rep-elem-of-tree-fix-cst

(defthm ocst-falseliteral-conc-rep-elem-of-tree-fix-cst
 (equal (ocst-falseliteral-conc-rep-elem (abnf::tree-fix abnf::cst))
        (ocst-falseliteral-conc-rep-elem abnf::cst)))

Theorem: ocst-falseliteral-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-falseliteral-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-falseliteral-conc-rep-elem abnf::cst)
                  (ocst-falseliteral-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: ocst-decimaldigit-conc-rep-elem

(defun ocst-decimaldigit-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (ocst-matchp abnf::cst "decimaldigit")))
  (let ((__function__ 'ocst-decimaldigit-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (ocst-decimaldigit-conc-rep abnf::cst)))))

Theorem: treep-of-ocst-decimaldigit-conc-rep-elem

(defthm treep-of-ocst-decimaldigit-conc-rep-elem
  (b* ((abnf::cst1 (ocst-decimaldigit-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: ocst-decimaldigit-conc-rep-elem-match

(defthm ocst-decimaldigit-conc-rep-elem-match
 (implies
      (ocst-matchp abnf::cst "decimaldigit")
      (b* ((abnf::cst1 (ocst-decimaldigit-conc-rep-elem abnf::cst)))
        (ocst-matchp abnf::cst1 "%x30-39")))
 :rule-classes :rewrite)

Theorem: ocst-decimaldigit-conc-rep-elem-of-tree-fix-cst

(defthm ocst-decimaldigit-conc-rep-elem-of-tree-fix-cst
 (equal (ocst-decimaldigit-conc-rep-elem (abnf::tree-fix abnf::cst))
        (ocst-decimaldigit-conc-rep-elem abnf::cst)))

Theorem: ocst-decimaldigit-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm ocst-decimaldigit-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (ocst-decimaldigit-conc-rep-elem abnf::cst)
                  (ocst-decimaldigit-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

*grammar-old*-tree-operations

Definitions and Theorems

grammar-old-tree-operations