		Search-engine friendly clone of the ACL2 documentation.

*all-grammar-rules*

all-grammar-rules-tree-operations

Tree operations specialized to *all-grammar-rules*.

Definitions and Theorems

Function: cst-matchp$

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

Theorem: booleanp-of-cst-matchp$

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

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

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

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

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

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

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

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

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

Function: cst-list-elem-matchp$

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

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

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

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

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

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

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

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

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

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

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

Function: cst-list-rep-matchp$

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

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

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

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

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

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

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

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

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

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

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

Function: cst-list-list-conc-matchp$

(defun cst-list-list-conc-matchp$ (abnf::treess abnf::conc)
  (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess)
                              (abnf::concatenationp abnf::conc))))
  (let ((__function__ 'cst-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 *all-grammar-rules*))))

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

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

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

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

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

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

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

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

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

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

Function: cst-list-list-alt-matchp$

(defun cst-list-list-alt-matchp$ (abnf::treess abnf::alt)
  (declare (xargs :guard (and (abnf::tree-list-listp abnf::treess)
                              (abnf::alternationp abnf::alt))))
  (let ((__function__ 'cst-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 *all-grammar-rules*))))

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

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

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

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

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

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

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

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

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

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

Function: cst-%x20-21-nat

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

Theorem: natp-of-cst-%x20-21-nat

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

Theorem: cst-%x20-21-nat-of-tree-fix-cst

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

Theorem: cst-%x20-21-nat-tree-equiv-congruence-on-cst

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

Function: cst-%x23-5b-nat

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

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

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

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

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

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

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

Function: cst-%x30-39-nat

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

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

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

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

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

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

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

Function: cst-%x31-39-nat

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

Theorem: natp-of-cst-%x31-39-nat

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

Theorem: cst-%x31-39-nat-of-tree-fix-cst

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

Theorem: cst-%x31-39-nat-tree-equiv-congruence-on-cst

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

Function: cst-%x5d-10ffff-nat

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

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

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

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

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

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

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

Theorem: cst-%x20-21-nat-bounds

(defthm cst-%x20-21-nat-bounds
  (implies (cst-matchp abnf::cst "%x20-21")
           (and (<= 32 (cst-%x20-21-nat abnf::cst))
                (<= (cst-%x20-21-nat abnf::cst) 33)))
  :rule-classes :linear)

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

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

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

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

Theorem: cst-%x31-39-nat-bounds

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

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

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

Theorem: cst-"a"-leafterm

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

Theorem: cst-"b"-leafterm

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

Theorem: cst-"c"-leafterm

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

Theorem: cst-"d"-leafterm

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

Theorem: cst-"e"-leafterm

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

Theorem: cst-"f"-leafterm

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

Theorem: cst-json-text-nonleaf

(defthm cst-json-text-nonleaf
  (implies (cst-matchp abnf::cst "json-text")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-begin-array-nonleaf

(defthm cst-begin-array-nonleaf
  (implies (cst-matchp abnf::cst "begin-array")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-begin-object-nonleaf

(defthm cst-begin-object-nonleaf
  (implies (cst-matchp abnf::cst "begin-object")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-end-array-nonleaf

(defthm cst-end-array-nonleaf
  (implies (cst-matchp abnf::cst "end-array")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-end-object-nonleaf

(defthm cst-end-object-nonleaf
  (implies (cst-matchp abnf::cst "end-object")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-name-separator-nonleaf

(defthm cst-name-separator-nonleaf
  (implies (cst-matchp abnf::cst "name-separator")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-value-separator-nonleaf

(defthm cst-value-separator-nonleaf
  (implies (cst-matchp abnf::cst "value-separator")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-ws-nonleaf

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

Theorem: cst-value-nonleaf

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

Theorem: cst-false-nonleaf

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

Theorem: cst-null-nonleaf

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

Theorem: cst-true-nonleaf

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

Theorem: cst-object-nonleaf

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

Theorem: cst-member-nonleaf

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

Theorem: cst-array-nonleaf

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

Theorem: cst-number-nonleaf

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

Theorem: cst-decimal-point-nonleaf

(defthm cst-decimal-point-nonleaf
  (implies (cst-matchp abnf::cst "decimal-point")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-digit1-9-nonleaf

(defthm cst-digit1-9-nonleaf
  (implies (cst-matchp abnf::cst "digit1-9")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-e-nonleaf

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

Theorem: cst-exp-nonleaf

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

Theorem: cst-frac-nonleaf

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

Theorem: cst-int-nonleaf

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

Theorem: cst-minus-nonleaf

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

Theorem: cst-plus-nonleaf

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

Theorem: cst-zero-nonleaf

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

Theorem: cst-string-nonleaf

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

Theorem: cst-char-nonleaf

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

Theorem: cst-escape-nonleaf

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

Theorem: cst-quotation-mark-nonleaf

(defthm cst-quotation-mark-nonleaf
  (implies (cst-matchp abnf::cst "quotation-mark")
           (equal (abnf::tree-kind abnf::cst)
                  :nonleaf)))

Theorem: cst-unescaped-nonleaf

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

Theorem: cst-digit-nonleaf

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

Theorem: cst-hexdig-nonleaf

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

Theorem: cst-json-text-rulename

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

Theorem: cst-begin-array-rulename

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

Theorem: cst-begin-object-rulename

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

Theorem: cst-end-array-rulename

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

Theorem: cst-end-object-rulename

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

Theorem: cst-name-separator-rulename

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

Theorem: cst-value-separator-rulename

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

Theorem: cst-ws-rulename

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

Theorem: cst-value-rulename

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

Theorem: cst-false-rulename

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

Theorem: cst-null-rulename

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

Theorem: cst-true-rulename

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

Theorem: cst-object-rulename

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

Theorem: cst-member-rulename

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

Theorem: cst-array-rulename

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

Theorem: cst-number-rulename

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

Theorem: cst-decimal-point-rulename

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

Theorem: cst-digit1-9-rulename

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

Theorem: cst-e-rulename

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

Theorem: cst-exp-rulename

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

Theorem: cst-frac-rulename

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

Theorem: cst-int-rulename

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

Theorem: cst-minus-rulename

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

Theorem: cst-plus-rulename

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

Theorem: cst-zero-rulename

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

Theorem: cst-string-rulename

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

Theorem: cst-char-rulename

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

Theorem: cst-escape-rulename

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

Theorem: cst-quotation-mark-rulename

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

Theorem: cst-unescaped-rulename

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

Theorem: cst-digit-rulename

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

Theorem: cst-hexdig-rulename

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

Theorem: cst-json-text-branches-match-alt

(defthm cst-json-text-branches-match-alt
 (implies
  (cst-matchp abnf::cst "json-text")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws value ws")))

Theorem: cst-begin-array-branches-match-alt

(defthm cst-begin-array-branches-match-alt
 (implies
  (cst-matchp abnf::cst "begin-array")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws %x5B ws")))

Theorem: cst-begin-object-branches-match-alt

(defthm cst-begin-object-branches-match-alt
 (implies
  (cst-matchp abnf::cst "begin-object")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws %x7B ws")))

Theorem: cst-end-array-branches-match-alt

(defthm cst-end-array-branches-match-alt
 (implies
  (cst-matchp abnf::cst "end-array")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws %x5D ws")))

Theorem: cst-end-object-branches-match-alt

(defthm cst-end-object-branches-match-alt
 (implies
  (cst-matchp abnf::cst "end-object")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws %x7D ws")))

Theorem: cst-name-separator-branches-match-alt

(defthm cst-name-separator-branches-match-alt
 (implies
  (cst-matchp abnf::cst "name-separator")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws %x3A ws")))

Theorem: cst-value-separator-branches-match-alt

(defthm cst-value-separator-branches-match-alt
 (implies
  (cst-matchp abnf::cst "value-separator")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "ws %x2C ws")))

Theorem: cst-ws-branches-match-alt

(defthm cst-ws-branches-match-alt
 (implies
  (cst-matchp abnf::cst "ws")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "*( %x20 / %x9 / %xA / %xD )")))

Theorem: cst-value-branches-match-alt

(defthm cst-value-branches-match-alt
 (implies
    (cst-matchp abnf::cst "value")
    (cst-list-list-alt-matchp
         (abnf::tree-nonleaf->branches abnf::cst)
         "false / null / true / object / array / number / string")))

Theorem: cst-false-branches-match-alt

(defthm cst-false-branches-match-alt
 (implies
  (cst-matchp abnf::cst "false")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x66.61.6C.73.65")))

Theorem: cst-null-branches-match-alt

(defthm cst-null-branches-match-alt
 (implies
  (cst-matchp abnf::cst "null")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x6E.75.6C.6C")))

Theorem: cst-true-branches-match-alt

(defthm cst-true-branches-match-alt
 (implies
  (cst-matchp abnf::cst "true")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x74.72.75.65")))

Theorem: cst-object-branches-match-alt

(defthm cst-object-branches-match-alt
 (implies
  (cst-matchp abnf::cst "object")
  (cst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "begin-object [ member *( value-separator member ) ] end-object")))

Theorem: cst-member-branches-match-alt

(defthm cst-member-branches-match-alt
 (implies
  (cst-matchp abnf::cst "member")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "string name-separator value")))

Theorem: cst-array-branches-match-alt

(defthm cst-array-branches-match-alt
 (implies
  (cst-matchp abnf::cst "array")
  (cst-list-list-alt-matchp
     (abnf::tree-nonleaf->branches abnf::cst)
     "begin-array [ value *( value-separator value ) ] end-array")))

Theorem: cst-number-branches-match-alt

(defthm cst-number-branches-match-alt
 (implies
  (cst-matchp abnf::cst "number")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "[ minus ] int [ frac ] [ exp ]")))

Theorem: cst-decimal-point-branches-match-alt

(defthm cst-decimal-point-branches-match-alt
 (implies
  (cst-matchp abnf::cst "decimal-point")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x2E")))

Theorem: cst-digit1-9-branches-match-alt

(defthm cst-digit1-9-branches-match-alt
 (implies
  (cst-matchp abnf::cst "digit1-9")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x31-39")))

Theorem: cst-e-branches-match-alt

(defthm cst-e-branches-match-alt
 (implies
  (cst-matchp abnf::cst "e")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x65 / %x45")))

Theorem: cst-exp-branches-match-alt

(defthm cst-exp-branches-match-alt
 (implies
  (cst-matchp abnf::cst "exp")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "e [ minus / plus ] 1*digit")))

Theorem: cst-frac-branches-match-alt

(defthm cst-frac-branches-match-alt
 (implies
  (cst-matchp abnf::cst "frac")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "decimal-point 1*digit")))

Theorem: cst-int-branches-match-alt

(defthm cst-int-branches-match-alt
 (implies
  (cst-matchp abnf::cst "int")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "zero / ( digit1-9 *digit )")))

Theorem: cst-minus-branches-match-alt

(defthm cst-minus-branches-match-alt
 (implies
  (cst-matchp abnf::cst "minus")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x2D")))

Theorem: cst-plus-branches-match-alt

(defthm cst-plus-branches-match-alt
 (implies
  (cst-matchp abnf::cst "plus")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x2B")))

Theorem: cst-zero-branches-match-alt

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

Theorem: cst-string-branches-match-alt

(defthm cst-string-branches-match-alt
 (implies
  (cst-matchp abnf::cst "string")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "quotation-mark *char quotation-mark")))

Theorem: cst-char-branches-match-alt

(defthm cst-char-branches-match-alt
 (implies
  (cst-matchp abnf::cst "char")
  (cst-list-list-alt-matchp
   (abnf::tree-nonleaf->branches abnf::cst)
   "unescaped / escape ( %x22 / %x5C / %x2F / %x62 / %x66 / %x6E / %x72 / %x74 / %x75 4hexdig )")))

Theorem: cst-escape-branches-match-alt

(defthm cst-escape-branches-match-alt
 (implies
  (cst-matchp abnf::cst "escape")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x5C")))

Theorem: cst-quotation-mark-branches-match-alt

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

Theorem: cst-unescaped-branches-match-alt

(defthm cst-unescaped-branches-match-alt
 (implies
  (cst-matchp abnf::cst "unescaped")
  (cst-list-list-alt-matchp (abnf::tree-nonleaf->branches abnf::cst)
                            "%x20-21 / %x23-5B / %x5D-10FFFF")))

Theorem: cst-digit-branches-match-alt

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

Theorem: cst-hexdig-branches-match-alt

(defthm cst-hexdig-branches-match-alt
  (implies (cst-matchp abnf::cst "hexdig")
           (cst-list-list-alt-matchp
                (abnf::tree-nonleaf->branches abnf::cst)
                "digit / \"A\" / \"B\" / \"C\" / \"D\" / \"E\" / \"F\"")))

Theorem: cst-json-text-concs

(defthm cst-json-text-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws value ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws value ws"))))

Theorem: cst-begin-array-concs

(defthm cst-begin-array-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws %x5B ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws %x5B ws"))))

Theorem: cst-begin-object-concs

(defthm cst-begin-object-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws %x7B ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws %x7B ws"))))

Theorem: cst-end-array-concs

(defthm cst-end-array-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws %x5D ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws %x5D ws"))))

Theorem: cst-end-object-concs

(defthm cst-end-object-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws %x7D ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws %x7D ws"))))

Theorem: cst-name-separator-concs

(defthm cst-name-separator-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws %x3A ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws %x3A ws"))))

Theorem: cst-value-separator-concs

(defthm cst-value-separator-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss "ws %x2C ws")
       (or (cst-list-list-conc-matchp abnf::cstss "ws %x2C ws"))))

Theorem: cst-ws-concs

(defthm cst-ws-concs
 (implies
    (cst-list-list-alt-matchp abnf::cstss
                              "*( %x20 / %x9 / %xA / %xD )")
    (or (cst-list-list-conc-matchp abnf::cstss
                                   "*( %x20 / %x9 / %xA / %xD )"))))

Theorem: cst-value-concs

(defthm cst-value-concs
 (implies
      (cst-list-list-alt-matchp
           abnf::cstss
           "false / null / true / object / array / number / string")
      (or (cst-list-list-conc-matchp abnf::cstss "false")
          (cst-list-list-conc-matchp abnf::cstss "null")
          (cst-list-list-conc-matchp abnf::cstss "true")
          (cst-list-list-conc-matchp abnf::cstss "object")
          (cst-list-list-conc-matchp abnf::cstss "array")
          (cst-list-list-conc-matchp abnf::cstss "number")
          (cst-list-list-conc-matchp abnf::cstss "string"))))

Theorem: cst-false-concs

(defthm cst-false-concs
 (implies
   (cst-list-list-alt-matchp abnf::cstss "%x66.61.6C.73.65")
   (or (cst-list-list-conc-matchp abnf::cstss "%x66.61.6C.73.65"))))

Theorem: cst-null-concs

(defthm cst-null-concs
 (implies
      (cst-list-list-alt-matchp abnf::cstss "%x6E.75.6C.6C")
      (or (cst-list-list-conc-matchp abnf::cstss "%x6E.75.6C.6C"))))

Theorem: cst-true-concs

(defthm cst-true-concs
 (implies
      (cst-list-list-alt-matchp abnf::cstss "%x74.72.75.65")
      (or (cst-list-list-conc-matchp abnf::cstss "%x74.72.75.65"))))

Theorem: cst-object-concs

(defthm cst-object-concs
 (implies
  (cst-list-list-alt-matchp
   abnf::cstss
   "begin-object [ member *( value-separator member ) ] end-object")
  (or
   (cst-list-list-conc-matchp
    abnf::cstss
    "begin-object [ member *( value-separator member ) ] end-object"))))

Theorem: cst-member-concs

(defthm cst-member-concs
 (implies
    (cst-list-list-alt-matchp abnf::cstss
                              "string name-separator value")
    (or (cst-list-list-conc-matchp abnf::cstss
                                   "string name-separator value"))))

Theorem: cst-array-concs

(defthm cst-array-concs
 (implies
  (cst-list-list-alt-matchp
       abnf::cstss
       "begin-array [ value *( value-separator value ) ] end-array")
  (or
   (cst-list-list-conc-matchp
    abnf::cstss
    "begin-array [ value *( value-separator value ) ] end-array"))))

Theorem: cst-number-concs

(defthm cst-number-concs
 (implies
  (cst-list-list-alt-matchp abnf::cstss
                            "[ minus ] int [ frac ] [ exp ]")
  (or
     (cst-list-list-conc-matchp abnf::cstss
                                "[ minus ] int [ frac ] [ exp ]"))))

Theorem: cst-decimal-point-concs

(defthm cst-decimal-point-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x2E")
           (or (cst-list-list-conc-matchp abnf::cstss "%x2E"))))

Theorem: cst-digit1-9-concs

(defthm cst-digit1-9-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x31-39")
           (or (cst-list-list-conc-matchp abnf::cstss "%x31-39"))))

Theorem: cst-e-concs

(defthm cst-e-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x65 / %x45")
           (or (cst-list-list-conc-matchp abnf::cstss "%x65")
               (cst-list-list-conc-matchp abnf::cstss "%x45"))))

Theorem: cst-exp-concs

(defthm cst-exp-concs
 (implies
     (cst-list-list-alt-matchp abnf::cstss
                               "e [ minus / plus ] 1*digit")
     (or (cst-list-list-conc-matchp abnf::cstss
                                    "e [ minus / plus ] 1*digit"))))

Theorem: cst-frac-concs

(defthm cst-frac-concs
 (implies
      (cst-list-list-alt-matchp abnf::cstss "decimal-point 1*digit")
      (or (cst-list-list-conc-matchp
               abnf::cstss "decimal-point 1*digit"))))

Theorem: cst-int-concs

(defthm cst-int-concs
 (implies
  (cst-list-list-alt-matchp abnf::cstss
                            "zero / ( digit1-9 *digit )")
  (or
    (cst-list-list-conc-matchp abnf::cstss "zero")
    (cst-list-list-conc-matchp abnf::cstss "( digit1-9 *digit )"))))

Theorem: cst-minus-concs

(defthm cst-minus-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x2D")
           (or (cst-list-list-conc-matchp abnf::cstss "%x2D"))))

Theorem: cst-plus-concs

(defthm cst-plus-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x2B")
           (or (cst-list-list-conc-matchp abnf::cstss "%x2B"))))

Theorem: cst-zero-concs

(defthm cst-zero-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x30")
           (or (cst-list-list-conc-matchp abnf::cstss "%x30"))))

Theorem: cst-string-concs

(defthm cst-string-concs
 (implies
    (cst-list-list-alt-matchp abnf::cstss
                              "quotation-mark *char quotation-mark")
    (or (cst-list-list-conc-matchp
             abnf::cstss
             "quotation-mark *char quotation-mark"))))

Theorem: cst-char-concs

(defthm cst-char-concs
 (implies
  (cst-list-list-alt-matchp
   abnf::cstss
   "unescaped / escape ( %x22 / %x5C / %x2F / %x62 / %x66 / %x6E / %x72 / %x74 / %x75 4hexdig )")
  (or
   (cst-list-list-conc-matchp abnf::cstss "unescaped")
   (cst-list-list-conc-matchp
    abnf::cstss
    "escape ( %x22 / %x5C / %x2F / %x62 / %x66 / %x6E / %x72 / %x74 / %x75 4hexdig )"))))

Theorem: cst-escape-concs

(defthm cst-escape-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x5C")
           (or (cst-list-list-conc-matchp abnf::cstss "%x5C"))))

Theorem: cst-quotation-mark-concs

(defthm cst-quotation-mark-concs
  (implies (cst-list-list-alt-matchp abnf::cstss "%x22")
           (or (cst-list-list-conc-matchp abnf::cstss "%x22"))))

Theorem: cst-unescaped-concs

(defthm cst-unescaped-concs
  (implies
       (cst-list-list-alt-matchp abnf::cstss
                                 "%x20-21 / %x23-5B / %x5D-10FFFF")
       (or (cst-list-list-conc-matchp abnf::cstss "%x20-21")
           (cst-list-list-conc-matchp abnf::cstss "%x23-5B")
           (cst-list-list-conc-matchp abnf::cstss "%x5D-10FFFF"))))

Theorem: cst-digit-concs

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

Theorem: cst-hexdig-concs

(defthm cst-hexdig-concs
  (implies (cst-list-list-alt-matchp
                abnf::cstss
                "digit / \"A\" / \"B\" / \"C\" / \"D\" / \"E\" / \"F\"")
           (or (cst-list-list-conc-matchp abnf::cstss "digit")
               (cst-list-list-conc-matchp abnf::cstss "\"A\"")
               (cst-list-list-conc-matchp abnf::cstss "\"B\"")
               (cst-list-list-conc-matchp abnf::cstss "\"C\"")
               (cst-list-list-conc-matchp abnf::cstss "\"D\"")
               (cst-list-list-conc-matchp abnf::cstss "\"E\"")
               (cst-list-list-conc-matchp abnf::cstss "\"F\""))))

Theorem: cst-ws-conc-matching

(defthm cst-ws-conc-matching
  (implies
       (cst-list-list-conc-matchp abnf::cstss
                                  "*( %x20 / %x9 / %xA / %xD )")
       (and (equal (len abnf::cstss) 1)
            (cst-list-rep-matchp (nth 0 abnf::cstss)
                                 "*( %x20 / %x9 / %xA / %xD )"))))

Theorem: cst-value-conc1-matching

(defthm cst-value-conc1-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "false")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "false"))))

Theorem: cst-value-conc2-matching

(defthm cst-value-conc2-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "null")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "null"))))

Theorem: cst-value-conc3-matching

(defthm cst-value-conc3-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "true")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "true"))))

Theorem: cst-value-conc4-matching

(defthm cst-value-conc4-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "object")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "object"))))

Theorem: cst-value-conc5-matching

(defthm cst-value-conc5-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "array")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "array"))))

Theorem: cst-value-conc6-matching

(defthm cst-value-conc6-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "number")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "number"))))

Theorem: cst-value-conc7-matching

(defthm cst-value-conc7-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "string")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "string"))))

Theorem: cst-false-conc-matching

(defthm cst-false-conc-matching
 (implies (cst-list-list-conc-matchp abnf::cstss "%x66.61.6C.73.65")
          (and (equal (len abnf::cstss) 1)
               (cst-list-rep-matchp (nth 0 abnf::cstss)
                                    "%x66.61.6C.73.65"))))

Theorem: cst-null-conc-matching

(defthm cst-null-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x6E.75.6C.6C")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x6E.75.6C.6C"))))

Theorem: cst-true-conc-matching

(defthm cst-true-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x74.72.75.65")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x74.72.75.65"))))

Theorem: cst-decimal-point-conc-matching

(defthm cst-decimal-point-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x2E")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x2E"))))

Theorem: cst-digit1-9-conc-matching

(defthm cst-digit1-9-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x31-39")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x31-39"))))

Theorem: cst-e-conc1-matching

(defthm cst-e-conc1-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x65")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x65"))))

Theorem: cst-e-conc2-matching

(defthm cst-e-conc2-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x45")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x45"))))

Theorem: cst-int-conc1-matching

(defthm cst-int-conc1-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "zero")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "zero"))))

Theorem: cst-int-conc2-matching

(defthm cst-int-conc2-matching
  (implies
       (cst-list-list-conc-matchp abnf::cstss "( digit1-9 *digit )")
       (and (equal (len abnf::cstss) 1)
            (cst-list-rep-matchp (nth 0 abnf::cstss)
                                 "( digit1-9 *digit )"))))

Theorem: cst-minus-conc-matching

(defthm cst-minus-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x2D")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x2D"))))

Theorem: cst-plus-conc-matching

(defthm cst-plus-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x2B")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x2B"))))

Theorem: cst-zero-conc-matching

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

Theorem: cst-char-conc1-matching

(defthm cst-char-conc1-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "unescaped")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "unescaped"))))

Theorem: cst-escape-conc-matching

(defthm cst-escape-conc-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x5C")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x5C"))))

Theorem: cst-quotation-mark-conc-matching

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

Theorem: cst-unescaped-conc1-matching

(defthm cst-unescaped-conc1-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x20-21")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x20-21"))))

Theorem: cst-unescaped-conc2-matching

(defthm cst-unescaped-conc2-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x23-5B")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x23-5B"))))

Theorem: cst-unescaped-conc3-matching

(defthm cst-unescaped-conc3-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "%x5D-10FFFF")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "%x5D-10FFFF"))))

Theorem: cst-digit-conc-matching

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

Theorem: cst-hexdig-conc1-matching

(defthm cst-hexdig-conc1-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "digit")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "digit"))))

Theorem: cst-hexdig-conc2-matching

(defthm cst-hexdig-conc2-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "\"A\"")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "\"A\""))))

Theorem: cst-hexdig-conc3-matching

(defthm cst-hexdig-conc3-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "\"B\"")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "\"B\""))))

Theorem: cst-hexdig-conc4-matching

(defthm cst-hexdig-conc4-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "\"C\"")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "\"C\""))))

Theorem: cst-hexdig-conc5-matching

(defthm cst-hexdig-conc5-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "\"D\"")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "\"D\""))))

Theorem: cst-hexdig-conc6-matching

(defthm cst-hexdig-conc6-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "\"E\"")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "\"E\""))))

Theorem: cst-hexdig-conc7-matching

(defthm cst-hexdig-conc7-matching
  (implies (cst-list-list-conc-matchp abnf::cstss "\"F\"")
           (and (equal (len abnf::cstss) 1)
                (cst-list-rep-matchp (nth 0 abnf::cstss)
                                     "\"F\""))))

Theorem: cst-value-conc1-rep-matching

(defthm cst-value-conc1-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "false")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "false"))))

Theorem: cst-value-conc2-rep-matching

(defthm cst-value-conc2-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "null")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "null"))))

Theorem: cst-value-conc3-rep-matching

(defthm cst-value-conc3-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "true")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "true"))))

Theorem: cst-value-conc4-rep-matching

(defthm cst-value-conc4-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "object")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "object"))))

Theorem: cst-value-conc5-rep-matching

(defthm cst-value-conc5-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "array")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "array"))))

Theorem: cst-value-conc6-rep-matching

(defthm cst-value-conc6-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "number")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "number"))))

Theorem: cst-value-conc7-rep-matching

(defthm cst-value-conc7-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "string")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "string"))))

Theorem: cst-false-conc-rep-matching

(defthm cst-false-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x66.61.6C.73.65")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x66.61.6C.73.65"))))

Theorem: cst-null-conc-rep-matching

(defthm cst-null-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x6E.75.6C.6C")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x6E.75.6C.6C"))))

Theorem: cst-true-conc-rep-matching

(defthm cst-true-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x74.72.75.65")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x74.72.75.65"))))

Theorem: cst-decimal-point-conc-rep-matching

(defthm cst-decimal-point-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x2E")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x2E"))))

Theorem: cst-digit1-9-conc-rep-matching

(defthm cst-digit1-9-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x31-39")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x31-39"))))

Theorem: cst-e-conc1-rep-matching

(defthm cst-e-conc1-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x65")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x65"))))

Theorem: cst-e-conc2-rep-matching

(defthm cst-e-conc2-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x45")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x45"))))

Theorem: cst-int-conc1-rep-matching

(defthm cst-int-conc1-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "zero")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "zero"))))

Theorem: cst-int-conc2-rep-matching

(defthm cst-int-conc2-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "( digit1-9 *digit )")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "( digit1-9 *digit )"))))

Theorem: cst-minus-conc-rep-matching

(defthm cst-minus-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x2D")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x2D"))))

Theorem: cst-plus-conc-rep-matching

(defthm cst-plus-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x2B")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x2B"))))

Theorem: cst-zero-conc-rep-matching

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

Theorem: cst-char-conc1-rep-matching

(defthm cst-char-conc1-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "unescaped")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "unescaped"))))

Theorem: cst-escape-conc-rep-matching

(defthm cst-escape-conc-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x5C")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x5C"))))

Theorem: cst-quotation-mark-conc-rep-matching

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

Theorem: cst-unescaped-conc1-rep-matching

(defthm cst-unescaped-conc1-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x20-21")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x20-21"))))

Theorem: cst-unescaped-conc2-rep-matching

(defthm cst-unescaped-conc2-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x23-5B")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x23-5B"))))

Theorem: cst-unescaped-conc3-rep-matching

(defthm cst-unescaped-conc3-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "%x5D-10FFFF")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "%x5D-10FFFF"))))

Theorem: cst-digit-conc-rep-matching

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

Theorem: cst-hexdig-conc1-rep-matching

(defthm cst-hexdig-conc1-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "digit")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts)
                            "digit"))))

Theorem: cst-hexdig-conc2-rep-matching

(defthm cst-hexdig-conc2-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "\"A\"")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts) "\"A\""))))

Theorem: cst-hexdig-conc3-rep-matching

(defthm cst-hexdig-conc3-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "\"B\"")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts) "\"B\""))))

Theorem: cst-hexdig-conc4-rep-matching

(defthm cst-hexdig-conc4-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "\"C\"")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts) "\"C\""))))

Theorem: cst-hexdig-conc5-rep-matching

(defthm cst-hexdig-conc5-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "\"D\"")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts) "\"D\""))))

Theorem: cst-hexdig-conc6-rep-matching

(defthm cst-hexdig-conc6-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "\"E\"")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts) "\"E\""))))

Theorem: cst-hexdig-conc7-rep-matching

(defthm cst-hexdig-conc7-rep-matching
  (implies (cst-list-rep-matchp abnf::csts "\"F\"")
           (and (equal (len abnf::csts) 1)
                (cst-matchp (nth 0 abnf::csts) "\"F\""))))

Theorem: cst-value-conc-equivs

(defthm cst-value-conc-equivs
 (implies
  (cst-matchp abnf::cst "value")
  (and
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "false")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "false")))
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "null")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "null")))
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "true")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "true")))
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "object")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "object")))
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "array")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "array")))
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "number")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "number")))
   (iff
     (cst-list-list-conc-matchp
          (abnf::tree-nonleaf->branches abnf::cst)
          "string")
     (equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "string"))))))

Function: cst-value-conc?

(defun cst-value-conc? (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (cst-matchp abnf::cst "value")))
 (let ((__function__ 'cst-value-conc?))
  (declare (ignorable __function__))
  (cond
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "false"))
     1)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "null"))
     2)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "true"))
     3)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "object"))
     4)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "array"))
     5)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "number"))
     6)
    ((equal
          (abnf::tree-nonleaf->rulename?
               (nth 0
                    (nth 0
                         (abnf::tree-nonleaf->branches abnf::cst))))
          (abnf::rulename "string"))
     7)
    (t (prog2$ (acl2::impossible) 1)))))

Theorem: posp-of-cst-value-conc?

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

Theorem: cst-value-conc?-possibilities

(defthm cst-value-conc?-possibilities
 (b* ((number (cst-value-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)))
 :rule-classes
 ((:forward-chaining :trigger-terms ((cst-value-conc? abnf::cst)))))

Theorem: cst-value-conc?-of-tree-fix-cst

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

Theorem: cst-value-conc?-tree-equiv-congruence-on-cst

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

Theorem: cst-value-conc?-1-iff-match-conc

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

Theorem: cst-value-conc?-2-iff-match-conc

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

Theorem: cst-value-conc?-3-iff-match-conc

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

Theorem: cst-value-conc?-4-iff-match-conc

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

Theorem: cst-value-conc?-5-iff-match-conc

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

Theorem: cst-value-conc?-6-iff-match-conc

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

Theorem: cst-value-conc?-7-iff-match-conc

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

Function: cst-json-text-conc

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

Theorem: tree-list-listp-of-cst-json-text-conc

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

Theorem: cst-json-text-conc-match

(defthm cst-json-text-conc-match
  (implies (cst-matchp abnf::cst "json-text")
           (b* ((abnf::cstss (cst-json-text-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws value ws")))
  :rule-classes :rewrite)

Theorem: cst-json-text-conc-of-tree-fix-cst

(defthm cst-json-text-conc-of-tree-fix-cst
  (equal (cst-json-text-conc (abnf::tree-fix abnf::cst))
         (cst-json-text-conc abnf::cst)))

Theorem: cst-json-text-conc-tree-equiv-congruence-on-cst

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

Function: cst-begin-array-conc

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

Theorem: tree-list-listp-of-cst-begin-array-conc

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

Theorem: cst-begin-array-conc-match

(defthm cst-begin-array-conc-match
  (implies (cst-matchp abnf::cst "begin-array")
           (b* ((abnf::cstss (cst-begin-array-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws %x5B ws")))
  :rule-classes :rewrite)

Theorem: cst-begin-array-conc-of-tree-fix-cst

(defthm cst-begin-array-conc-of-tree-fix-cst
  (equal (cst-begin-array-conc (abnf::tree-fix abnf::cst))
         (cst-begin-array-conc abnf::cst)))

Theorem: cst-begin-array-conc-tree-equiv-congruence-on-cst

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

Function: cst-begin-object-conc

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

Theorem: tree-list-listp-of-cst-begin-object-conc

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

Theorem: cst-begin-object-conc-match

(defthm cst-begin-object-conc-match
  (implies (cst-matchp abnf::cst "begin-object")
           (b* ((abnf::cstss (cst-begin-object-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws %x7B ws")))
  :rule-classes :rewrite)

Theorem: cst-begin-object-conc-of-tree-fix-cst

(defthm cst-begin-object-conc-of-tree-fix-cst
  (equal (cst-begin-object-conc (abnf::tree-fix abnf::cst))
         (cst-begin-object-conc abnf::cst)))

Theorem: cst-begin-object-conc-tree-equiv-congruence-on-cst

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

Function: cst-end-array-conc

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

Theorem: tree-list-listp-of-cst-end-array-conc

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

Theorem: cst-end-array-conc-match

(defthm cst-end-array-conc-match
  (implies (cst-matchp abnf::cst "end-array")
           (b* ((abnf::cstss (cst-end-array-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws %x5D ws")))
  :rule-classes :rewrite)

Theorem: cst-end-array-conc-of-tree-fix-cst

(defthm cst-end-array-conc-of-tree-fix-cst
  (equal (cst-end-array-conc (abnf::tree-fix abnf::cst))
         (cst-end-array-conc abnf::cst)))

Theorem: cst-end-array-conc-tree-equiv-congruence-on-cst

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

Function: cst-end-object-conc

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

Theorem: tree-list-listp-of-cst-end-object-conc

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

Theorem: cst-end-object-conc-match

(defthm cst-end-object-conc-match
  (implies (cst-matchp abnf::cst "end-object")
           (b* ((abnf::cstss (cst-end-object-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws %x7D ws")))
  :rule-classes :rewrite)

Theorem: cst-end-object-conc-of-tree-fix-cst

(defthm cst-end-object-conc-of-tree-fix-cst
  (equal (cst-end-object-conc (abnf::tree-fix abnf::cst))
         (cst-end-object-conc abnf::cst)))

Theorem: cst-end-object-conc-tree-equiv-congruence-on-cst

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

Function: cst-name-separator-conc

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

Theorem: tree-list-listp-of-cst-name-separator-conc

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

Theorem: cst-name-separator-conc-match

(defthm cst-name-separator-conc-match
  (implies (cst-matchp abnf::cst "name-separator")
           (b* ((abnf::cstss (cst-name-separator-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws %x3A ws")))
  :rule-classes :rewrite)

Theorem: cst-name-separator-conc-of-tree-fix-cst

(defthm cst-name-separator-conc-of-tree-fix-cst
  (equal (cst-name-separator-conc (abnf::tree-fix abnf::cst))
         (cst-name-separator-conc abnf::cst)))

Theorem: cst-name-separator-conc-tree-equiv-congruence-on-cst

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

Function: cst-value-separator-conc

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

Theorem: tree-list-listp-of-cst-value-separator-conc

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

Theorem: cst-value-separator-conc-match

(defthm cst-value-separator-conc-match
  (implies (cst-matchp abnf::cst "value-separator")
           (b* ((abnf::cstss (cst-value-separator-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "ws %x2C ws")))
  :rule-classes :rewrite)

Theorem: cst-value-separator-conc-of-tree-fix-cst

(defthm cst-value-separator-conc-of-tree-fix-cst
  (equal (cst-value-separator-conc (abnf::tree-fix abnf::cst))
         (cst-value-separator-conc abnf::cst)))

Theorem: cst-value-separator-conc-tree-equiv-congruence-on-cst

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

Function: cst-ws-conc

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

Theorem: tree-list-listp-of-cst-ws-conc

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

Theorem: cst-ws-conc-match

(defthm cst-ws-conc-match
  (implies
       (cst-matchp abnf::cst "ws")
       (b* ((abnf::cstss (cst-ws-conc abnf::cst)))
         (cst-list-list-conc-matchp abnf::cstss
                                    "*( %x20 / %x9 / %xA / %xD )")))
  :rule-classes :rewrite)

Theorem: cst-ws-conc-of-tree-fix-cst

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

Theorem: cst-ws-conc-tree-equiv-congruence-on-cst

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

Function: cst-value-conc1

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

Theorem: tree-list-listp-of-cst-value-conc1

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

Theorem: cst-value-conc1-match

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

Theorem: cst-value-conc1-of-tree-fix-cst

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

Theorem: cst-value-conc1-tree-equiv-congruence-on-cst

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

Function: cst-value-conc2

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

Theorem: tree-list-listp-of-cst-value-conc2

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

Theorem: cst-value-conc2-match

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

Theorem: cst-value-conc2-of-tree-fix-cst

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

Theorem: cst-value-conc2-tree-equiv-congruence-on-cst

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

Function: cst-value-conc3

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

Theorem: tree-list-listp-of-cst-value-conc3

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

Theorem: cst-value-conc3-match

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

Theorem: cst-value-conc3-of-tree-fix-cst

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

Theorem: cst-value-conc3-tree-equiv-congruence-on-cst

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

Function: cst-value-conc4

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

Theorem: tree-list-listp-of-cst-value-conc4

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

Theorem: cst-value-conc4-match

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

Theorem: cst-value-conc4-of-tree-fix-cst

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

Theorem: cst-value-conc4-tree-equiv-congruence-on-cst

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

Function: cst-value-conc5

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

Theorem: tree-list-listp-of-cst-value-conc5

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

Theorem: cst-value-conc5-match

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

Theorem: cst-value-conc5-of-tree-fix-cst

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

Theorem: cst-value-conc5-tree-equiv-congruence-on-cst

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

Function: cst-value-conc6

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

Theorem: tree-list-listp-of-cst-value-conc6

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

Theorem: cst-value-conc6-match

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

Theorem: cst-value-conc6-of-tree-fix-cst

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

Theorem: cst-value-conc6-tree-equiv-congruence-on-cst

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

Function: cst-value-conc7

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

Theorem: tree-list-listp-of-cst-value-conc7

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

Theorem: cst-value-conc7-match

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

Theorem: cst-value-conc7-of-tree-fix-cst

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

Theorem: cst-value-conc7-tree-equiv-congruence-on-cst

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

Function: cst-false-conc

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

Theorem: tree-list-listp-of-cst-false-conc

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

Theorem: cst-false-conc-match

(defthm cst-false-conc-match
 (implies
      (cst-matchp abnf::cst "false")
      (b* ((abnf::cstss (cst-false-conc abnf::cst)))
        (cst-list-list-conc-matchp abnf::cstss "%x66.61.6C.73.65")))
 :rule-classes :rewrite)

Theorem: cst-false-conc-of-tree-fix-cst

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

Theorem: cst-false-conc-tree-equiv-congruence-on-cst

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

Function: cst-null-conc

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

Theorem: tree-list-listp-of-cst-null-conc

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

Theorem: cst-null-conc-match

(defthm cst-null-conc-match
  (implies
       (cst-matchp abnf::cst "null")
       (b* ((abnf::cstss (cst-null-conc abnf::cst)))
         (cst-list-list-conc-matchp abnf::cstss "%x6E.75.6C.6C")))
  :rule-classes :rewrite)

Theorem: cst-null-conc-of-tree-fix-cst

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

Theorem: cst-null-conc-tree-equiv-congruence-on-cst

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

Function: cst-true-conc

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

Theorem: tree-list-listp-of-cst-true-conc

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

Theorem: cst-true-conc-match

(defthm cst-true-conc-match
  (implies
       (cst-matchp abnf::cst "true")
       (b* ((abnf::cstss (cst-true-conc abnf::cst)))
         (cst-list-list-conc-matchp abnf::cstss "%x74.72.75.65")))
  :rule-classes :rewrite)

Theorem: cst-true-conc-of-tree-fix-cst

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

Theorem: cst-true-conc-tree-equiv-congruence-on-cst

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

Function: cst-object-conc

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

Theorem: tree-list-listp-of-cst-object-conc

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

Theorem: cst-object-conc-match

(defthm cst-object-conc-match
 (implies
  (cst-matchp abnf::cst "object")
  (b* ((abnf::cstss (cst-object-conc abnf::cst)))
   (cst-list-list-conc-matchp
    abnf::cstss
    "begin-object [ member *( value-separator member ) ] end-object")))
 :rule-classes :rewrite)

Theorem: cst-object-conc-of-tree-fix-cst

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

Theorem: cst-object-conc-tree-equiv-congruence-on-cst

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

Function: cst-member-conc

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

Theorem: tree-list-listp-of-cst-member-conc

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

Theorem: cst-member-conc-match

(defthm cst-member-conc-match
  (implies
       (cst-matchp abnf::cst "member")
       (b* ((abnf::cstss (cst-member-conc abnf::cst)))
         (cst-list-list-conc-matchp abnf::cstss
                                    "string name-separator value")))
  :rule-classes :rewrite)

Theorem: cst-member-conc-of-tree-fix-cst

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

Theorem: cst-member-conc-tree-equiv-congruence-on-cst

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

Function: cst-array-conc

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

Theorem: tree-list-listp-of-cst-array-conc

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

Theorem: cst-array-conc-match

(defthm cst-array-conc-match
 (implies
  (cst-matchp abnf::cst "array")
  (b* ((abnf::cstss (cst-array-conc abnf::cst)))
   (cst-list-list-conc-matchp
     abnf::cstss
     "begin-array [ value *( value-separator value ) ] end-array")))
 :rule-classes :rewrite)

Theorem: cst-array-conc-of-tree-fix-cst

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

Theorem: cst-array-conc-tree-equiv-congruence-on-cst

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

Function: cst-number-conc

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

Theorem: tree-list-listp-of-cst-number-conc

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

Theorem: cst-number-conc-match

(defthm cst-number-conc-match
 (implies
    (cst-matchp abnf::cst "number")
    (b* ((abnf::cstss (cst-number-conc abnf::cst)))
      (cst-list-list-conc-matchp abnf::cstss
                                 "[ minus ] int [ frac ] [ exp ]")))
 :rule-classes :rewrite)

Theorem: cst-number-conc-of-tree-fix-cst

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

Theorem: cst-number-conc-tree-equiv-congruence-on-cst

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

Function: cst-decimal-point-conc

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

Theorem: tree-list-listp-of-cst-decimal-point-conc

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

Theorem: cst-decimal-point-conc-match

(defthm cst-decimal-point-conc-match
  (implies (cst-matchp abnf::cst "decimal-point")
           (b* ((abnf::cstss (cst-decimal-point-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "%x2E")))
  :rule-classes :rewrite)

Theorem: cst-decimal-point-conc-of-tree-fix-cst

(defthm cst-decimal-point-conc-of-tree-fix-cst
  (equal (cst-decimal-point-conc (abnf::tree-fix abnf::cst))
         (cst-decimal-point-conc abnf::cst)))

Theorem: cst-decimal-point-conc-tree-equiv-congruence-on-cst

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

Function: cst-digit1-9-conc

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

Theorem: tree-list-listp-of-cst-digit1-9-conc

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

Theorem: cst-digit1-9-conc-match

(defthm cst-digit1-9-conc-match
  (implies (cst-matchp abnf::cst "digit1-9")
           (b* ((abnf::cstss (cst-digit1-9-conc abnf::cst)))
             (cst-list-list-conc-matchp abnf::cstss "%x31-39")))
  :rule-classes :rewrite)

Theorem: cst-digit1-9-conc-of-tree-fix-cst

(defthm cst-digit1-9-conc-of-tree-fix-cst
  (equal (cst-digit1-9-conc (abnf::tree-fix abnf::cst))
         (cst-digit1-9-conc abnf::cst)))

Theorem: cst-digit1-9-conc-tree-equiv-congruence-on-cst

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

Function: cst-exp-conc

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

Theorem: tree-list-listp-of-cst-exp-conc

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

Theorem: cst-exp-conc-match

(defthm cst-exp-conc-match
  (implies
       (cst-matchp abnf::cst "exp")
       (b* ((abnf::cstss (cst-exp-conc abnf::cst)))
         (cst-list-list-conc-matchp abnf::cstss
                                    "e [ minus / plus ] 1*digit")))
  :rule-classes :rewrite)

Theorem: cst-exp-conc-of-tree-fix-cst

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

Theorem: cst-exp-conc-tree-equiv-congruence-on-cst

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

Function: cst-frac-conc

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

Theorem: tree-list-listp-of-cst-frac-conc

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

Theorem: cst-frac-conc-match

(defthm cst-frac-conc-match
 (implies
  (cst-matchp abnf::cst "frac")
  (b* ((abnf::cstss (cst-frac-conc abnf::cst)))
   (cst-list-list-conc-matchp abnf::cstss "decimal-point 1*digit")))
 :rule-classes :rewrite)

Theorem: cst-frac-conc-of-tree-fix-cst

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

Theorem: cst-frac-conc-tree-equiv-congruence-on-cst

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

Function: cst-minus-conc

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

Theorem: tree-list-listp-of-cst-minus-conc

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

Theorem: cst-minus-conc-match

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

Theorem: cst-minus-conc-of-tree-fix-cst

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

Theorem: cst-minus-conc-tree-equiv-congruence-on-cst

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

Function: cst-plus-conc

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

Theorem: tree-list-listp-of-cst-plus-conc

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

Theorem: cst-plus-conc-match

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

Theorem: cst-plus-conc-of-tree-fix-cst

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

Theorem: cst-plus-conc-tree-equiv-congruence-on-cst

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

Function: cst-zero-conc

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

Theorem: tree-list-listp-of-cst-zero-conc

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

Theorem: cst-zero-conc-match

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

Theorem: cst-zero-conc-of-tree-fix-cst

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

Theorem: cst-zero-conc-tree-equiv-congruence-on-cst

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

Function: cst-string-conc

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

Theorem: tree-list-listp-of-cst-string-conc

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

Theorem: cst-string-conc-match

(defthm cst-string-conc-match
  (implies (cst-matchp abnf::cst "string")
           (b* ((abnf::cstss (cst-string-conc abnf::cst)))
             (cst-list-list-conc-matchp
                  abnf::cstss
                  "quotation-mark *char quotation-mark")))
  :rule-classes :rewrite)

Theorem: cst-string-conc-of-tree-fix-cst

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

Theorem: cst-string-conc-tree-equiv-congruence-on-cst

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

Function: cst-escape-conc

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

Theorem: tree-list-listp-of-cst-escape-conc

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

Theorem: cst-escape-conc-match

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

Theorem: cst-escape-conc-of-tree-fix-cst

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

Theorem: cst-escape-conc-tree-equiv-congruence-on-cst

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

Function: cst-quotation-mark-conc

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

Theorem: tree-list-listp-of-cst-quotation-mark-conc

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

Theorem: cst-quotation-mark-conc-match

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

Theorem: cst-quotation-mark-conc-of-tree-fix-cst

(defthm cst-quotation-mark-conc-of-tree-fix-cst
  (equal (cst-quotation-mark-conc (abnf::tree-fix abnf::cst))
         (cst-quotation-mark-conc abnf::cst)))

Theorem: cst-quotation-mark-conc-tree-equiv-congruence-on-cst

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

Function: cst-digit-conc

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

Theorem: tree-list-listp-of-cst-digit-conc

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

Theorem: cst-digit-conc-match

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

Theorem: cst-digit-conc-of-tree-fix-cst

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

Theorem: cst-digit-conc-tree-equiv-congruence-on-cst

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

Function: cst-value-conc1-rep

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

Theorem: tree-listp-of-cst-value-conc1-rep

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

Theorem: cst-value-conc1-rep-match

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

Theorem: cst-value-conc1-rep-of-tree-fix-cst

(defthm cst-value-conc1-rep-of-tree-fix-cst
  (equal (cst-value-conc1-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc1-rep abnf::cst)))

Theorem: cst-value-conc1-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc2-rep

(defun cst-value-conc2-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 2))))
  (let ((__function__ 'cst-value-conc2-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-value-conc2 abnf::cst)))))

Theorem: tree-listp-of-cst-value-conc2-rep

(defthm tree-listp-of-cst-value-conc2-rep
  (b* ((abnf::csts (cst-value-conc2-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-value-conc2-rep-match

(defthm cst-value-conc2-rep-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 2))
           (b* ((abnf::csts (cst-value-conc2-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "null")))
  :rule-classes :rewrite)

Theorem: cst-value-conc2-rep-of-tree-fix-cst

(defthm cst-value-conc2-rep-of-tree-fix-cst
  (equal (cst-value-conc2-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc2-rep abnf::cst)))

Theorem: cst-value-conc2-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc3-rep

(defun cst-value-conc3-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 3))))
  (let ((__function__ 'cst-value-conc3-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-value-conc3 abnf::cst)))))

Theorem: tree-listp-of-cst-value-conc3-rep

(defthm tree-listp-of-cst-value-conc3-rep
  (b* ((abnf::csts (cst-value-conc3-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-value-conc3-rep-match

(defthm cst-value-conc3-rep-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 3))
           (b* ((abnf::csts (cst-value-conc3-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "true")))
  :rule-classes :rewrite)

Theorem: cst-value-conc3-rep-of-tree-fix-cst

(defthm cst-value-conc3-rep-of-tree-fix-cst
  (equal (cst-value-conc3-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc3-rep abnf::cst)))

Theorem: cst-value-conc3-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc4-rep

(defun cst-value-conc4-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 4))))
  (let ((__function__ 'cst-value-conc4-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-value-conc4 abnf::cst)))))

Theorem: tree-listp-of-cst-value-conc4-rep

(defthm tree-listp-of-cst-value-conc4-rep
  (b* ((abnf::csts (cst-value-conc4-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-value-conc4-rep-match

(defthm cst-value-conc4-rep-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 4))
           (b* ((abnf::csts (cst-value-conc4-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "object")))
  :rule-classes :rewrite)

Theorem: cst-value-conc4-rep-of-tree-fix-cst

(defthm cst-value-conc4-rep-of-tree-fix-cst
  (equal (cst-value-conc4-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc4-rep abnf::cst)))

Theorem: cst-value-conc4-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc5-rep

(defun cst-value-conc5-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 5))))
  (let ((__function__ 'cst-value-conc5-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-value-conc5 abnf::cst)))))

Theorem: tree-listp-of-cst-value-conc5-rep

(defthm tree-listp-of-cst-value-conc5-rep
  (b* ((abnf::csts (cst-value-conc5-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-value-conc5-rep-match

(defthm cst-value-conc5-rep-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 5))
           (b* ((abnf::csts (cst-value-conc5-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "array")))
  :rule-classes :rewrite)

Theorem: cst-value-conc5-rep-of-tree-fix-cst

(defthm cst-value-conc5-rep-of-tree-fix-cst
  (equal (cst-value-conc5-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc5-rep abnf::cst)))

Theorem: cst-value-conc5-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc6-rep

(defun cst-value-conc6-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 6))))
  (let ((__function__ 'cst-value-conc6-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-value-conc6 abnf::cst)))))

Theorem: tree-listp-of-cst-value-conc6-rep

(defthm tree-listp-of-cst-value-conc6-rep
  (b* ((abnf::csts (cst-value-conc6-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-value-conc6-rep-match

(defthm cst-value-conc6-rep-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 6))
           (b* ((abnf::csts (cst-value-conc6-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "number")))
  :rule-classes :rewrite)

Theorem: cst-value-conc6-rep-of-tree-fix-cst

(defthm cst-value-conc6-rep-of-tree-fix-cst
  (equal (cst-value-conc6-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc6-rep abnf::cst)))

Theorem: cst-value-conc6-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc7-rep

(defun cst-value-conc7-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 7))))
  (let ((__function__ 'cst-value-conc7-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-value-conc7 abnf::cst)))))

Theorem: tree-listp-of-cst-value-conc7-rep

(defthm tree-listp-of-cst-value-conc7-rep
  (b* ((abnf::csts (cst-value-conc7-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-value-conc7-rep-match

(defthm cst-value-conc7-rep-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 7))
           (b* ((abnf::csts (cst-value-conc7-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "string")))
  :rule-classes :rewrite)

Theorem: cst-value-conc7-rep-of-tree-fix-cst

(defthm cst-value-conc7-rep-of-tree-fix-cst
  (equal (cst-value-conc7-rep (abnf::tree-fix abnf::cst))
         (cst-value-conc7-rep abnf::cst)))

Theorem: cst-value-conc7-rep-tree-equiv-congruence-on-cst

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

Function: cst-false-conc-rep

(defun cst-false-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "false")))
  (let ((__function__ 'cst-false-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-false-conc abnf::cst)))))

Theorem: tree-listp-of-cst-false-conc-rep

(defthm tree-listp-of-cst-false-conc-rep
  (b* ((abnf::csts (cst-false-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-false-conc-rep-match

(defthm cst-false-conc-rep-match
  (implies (cst-matchp abnf::cst "false")
           (b* ((abnf::csts (cst-false-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x66.61.6C.73.65")))
  :rule-classes :rewrite)

Theorem: cst-false-conc-rep-of-tree-fix-cst

(defthm cst-false-conc-rep-of-tree-fix-cst
  (equal (cst-false-conc-rep (abnf::tree-fix abnf::cst))
         (cst-false-conc-rep abnf::cst)))

Theorem: cst-false-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-null-conc-rep

(defun cst-null-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "null")))
  (let ((__function__ 'cst-null-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-null-conc abnf::cst)))))

Theorem: tree-listp-of-cst-null-conc-rep

(defthm tree-listp-of-cst-null-conc-rep
  (b* ((abnf::csts (cst-null-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-null-conc-rep-match

(defthm cst-null-conc-rep-match
  (implies (cst-matchp abnf::cst "null")
           (b* ((abnf::csts (cst-null-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x6E.75.6C.6C")))
  :rule-classes :rewrite)

Theorem: cst-null-conc-rep-of-tree-fix-cst

(defthm cst-null-conc-rep-of-tree-fix-cst
  (equal (cst-null-conc-rep (abnf::tree-fix abnf::cst))
         (cst-null-conc-rep abnf::cst)))

Theorem: cst-null-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-true-conc-rep

(defun cst-true-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "true")))
  (let ((__function__ 'cst-true-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-true-conc abnf::cst)))))

Theorem: tree-listp-of-cst-true-conc-rep

(defthm tree-listp-of-cst-true-conc-rep
  (b* ((abnf::csts (cst-true-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-true-conc-rep-match

(defthm cst-true-conc-rep-match
  (implies (cst-matchp abnf::cst "true")
           (b* ((abnf::csts (cst-true-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x74.72.75.65")))
  :rule-classes :rewrite)

Theorem: cst-true-conc-rep-of-tree-fix-cst

(defthm cst-true-conc-rep-of-tree-fix-cst
  (equal (cst-true-conc-rep (abnf::tree-fix abnf::cst))
         (cst-true-conc-rep abnf::cst)))

Theorem: cst-true-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-decimal-point-conc-rep

(defun cst-decimal-point-conc-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (cst-matchp abnf::cst "decimal-point")))
 (let ((__function__ 'cst-decimal-point-conc-rep))
  (declare (ignorable __function__))
  (abnf::tree-list-fix (nth 0 (cst-decimal-point-conc abnf::cst)))))

Theorem: tree-listp-of-cst-decimal-point-conc-rep

(defthm tree-listp-of-cst-decimal-point-conc-rep
  (b* ((abnf::csts (cst-decimal-point-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-decimal-point-conc-rep-match

(defthm cst-decimal-point-conc-rep-match
  (implies (cst-matchp abnf::cst "decimal-point")
           (b* ((abnf::csts (cst-decimal-point-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x2E")))
  :rule-classes :rewrite)

Theorem: cst-decimal-point-conc-rep-of-tree-fix-cst

(defthm cst-decimal-point-conc-rep-of-tree-fix-cst
  (equal (cst-decimal-point-conc-rep (abnf::tree-fix abnf::cst))
         (cst-decimal-point-conc-rep abnf::cst)))

Theorem: cst-decimal-point-conc-rep-tree-equiv-congruence-on-cst

(defthm cst-decimal-point-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-decimal-point-conc-rep abnf::cst)
                  (cst-decimal-point-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: cst-digit1-9-conc-rep

(defun cst-digit1-9-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "digit1-9")))
  (let ((__function__ 'cst-digit1-9-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-digit1-9-conc abnf::cst)))))

Theorem: tree-listp-of-cst-digit1-9-conc-rep

(defthm tree-listp-of-cst-digit1-9-conc-rep
  (b* ((abnf::csts (cst-digit1-9-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-digit1-9-conc-rep-match

(defthm cst-digit1-9-conc-rep-match
  (implies (cst-matchp abnf::cst "digit1-9")
           (b* ((abnf::csts (cst-digit1-9-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x31-39")))
  :rule-classes :rewrite)

Theorem: cst-digit1-9-conc-rep-of-tree-fix-cst

(defthm cst-digit1-9-conc-rep-of-tree-fix-cst
  (equal (cst-digit1-9-conc-rep (abnf::tree-fix abnf::cst))
         (cst-digit1-9-conc-rep abnf::cst)))

Theorem: cst-digit1-9-conc-rep-tree-equiv-congruence-on-cst

(defthm cst-digit1-9-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-digit1-9-conc-rep abnf::cst)
                  (cst-digit1-9-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: cst-minus-conc-rep

(defun cst-minus-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "minus")))
  (let ((__function__ 'cst-minus-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-minus-conc abnf::cst)))))

Theorem: tree-listp-of-cst-minus-conc-rep

(defthm tree-listp-of-cst-minus-conc-rep
  (b* ((abnf::csts (cst-minus-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-minus-conc-rep-match

(defthm cst-minus-conc-rep-match
  (implies (cst-matchp abnf::cst "minus")
           (b* ((abnf::csts (cst-minus-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x2D")))
  :rule-classes :rewrite)

Theorem: cst-minus-conc-rep-of-tree-fix-cst

(defthm cst-minus-conc-rep-of-tree-fix-cst
  (equal (cst-minus-conc-rep (abnf::tree-fix abnf::cst))
         (cst-minus-conc-rep abnf::cst)))

Theorem: cst-minus-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-plus-conc-rep

(defun cst-plus-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "plus")))
  (let ((__function__ 'cst-plus-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-plus-conc abnf::cst)))))

Theorem: tree-listp-of-cst-plus-conc-rep

(defthm tree-listp-of-cst-plus-conc-rep
  (b* ((abnf::csts (cst-plus-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-plus-conc-rep-match

(defthm cst-plus-conc-rep-match
  (implies (cst-matchp abnf::cst "plus")
           (b* ((abnf::csts (cst-plus-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x2B")))
  :rule-classes :rewrite)

Theorem: cst-plus-conc-rep-of-tree-fix-cst

(defthm cst-plus-conc-rep-of-tree-fix-cst
  (equal (cst-plus-conc-rep (abnf::tree-fix abnf::cst))
         (cst-plus-conc-rep abnf::cst)))

Theorem: cst-plus-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-zero-conc-rep

(defun cst-zero-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "zero")))
  (let ((__function__ 'cst-zero-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-zero-conc abnf::cst)))))

Theorem: tree-listp-of-cst-zero-conc-rep

(defthm tree-listp-of-cst-zero-conc-rep
  (b* ((abnf::csts (cst-zero-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-zero-conc-rep-match

(defthm cst-zero-conc-rep-match
  (implies (cst-matchp abnf::cst "zero")
           (b* ((abnf::csts (cst-zero-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x30")))
  :rule-classes :rewrite)

Theorem: cst-zero-conc-rep-of-tree-fix-cst

(defthm cst-zero-conc-rep-of-tree-fix-cst
  (equal (cst-zero-conc-rep (abnf::tree-fix abnf::cst))
         (cst-zero-conc-rep abnf::cst)))

Theorem: cst-zero-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-escape-conc-rep

(defun cst-escape-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "escape")))
  (let ((__function__ 'cst-escape-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-escape-conc abnf::cst)))))

Theorem: tree-listp-of-cst-escape-conc-rep

(defthm tree-listp-of-cst-escape-conc-rep
  (b* ((abnf::csts (cst-escape-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-escape-conc-rep-match

(defthm cst-escape-conc-rep-match
  (implies (cst-matchp abnf::cst "escape")
           (b* ((abnf::csts (cst-escape-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x5C")))
  :rule-classes :rewrite)

Theorem: cst-escape-conc-rep-of-tree-fix-cst

(defthm cst-escape-conc-rep-of-tree-fix-cst
  (equal (cst-escape-conc-rep (abnf::tree-fix abnf::cst))
         (cst-escape-conc-rep abnf::cst)))

Theorem: cst-escape-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-quotation-mark-conc-rep

(defun cst-quotation-mark-conc-rep (abnf::cst)
 (declare (xargs :guard (abnf::treep abnf::cst)))
 (declare (xargs :guard (cst-matchp abnf::cst "quotation-mark")))
 (let ((__function__ 'cst-quotation-mark-conc-rep))
   (declare (ignorable __function__))
   (abnf::tree-list-fix (nth 0
                             (cst-quotation-mark-conc abnf::cst)))))

Theorem: tree-listp-of-cst-quotation-mark-conc-rep

(defthm tree-listp-of-cst-quotation-mark-conc-rep
  (b* ((abnf::csts (cst-quotation-mark-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-quotation-mark-conc-rep-match

(defthm cst-quotation-mark-conc-rep-match
 (implies (cst-matchp abnf::cst "quotation-mark")
          (b* ((abnf::csts (cst-quotation-mark-conc-rep abnf::cst)))
            (cst-list-rep-matchp abnf::csts "%x22")))
 :rule-classes :rewrite)

Theorem: cst-quotation-mark-conc-rep-of-tree-fix-cst

(defthm cst-quotation-mark-conc-rep-of-tree-fix-cst
  (equal (cst-quotation-mark-conc-rep (abnf::tree-fix abnf::cst))
         (cst-quotation-mark-conc-rep abnf::cst)))

Theorem: cst-quotation-mark-conc-rep-tree-equiv-congruence-on-cst

(defthm cst-quotation-mark-conc-rep-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-quotation-mark-conc-rep abnf::cst)
                  (cst-quotation-mark-conc-rep cst-equiv)))
  :rule-classes :congruence)

Function: cst-digit-conc-rep

(defun cst-digit-conc-rep (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "digit")))
  (let ((__function__ 'cst-digit-conc-rep))
    (declare (ignorable __function__))
    (abnf::tree-list-fix (nth 0 (cst-digit-conc abnf::cst)))))

Theorem: tree-listp-of-cst-digit-conc-rep

(defthm tree-listp-of-cst-digit-conc-rep
  (b* ((abnf::csts (cst-digit-conc-rep abnf::cst)))
    (abnf::tree-listp abnf::csts))
  :rule-classes :rewrite)

Theorem: cst-digit-conc-rep-match

(defthm cst-digit-conc-rep-match
  (implies (cst-matchp abnf::cst "digit")
           (b* ((abnf::csts (cst-digit-conc-rep abnf::cst)))
             (cst-list-rep-matchp abnf::csts "%x30-39")))
  :rule-classes :rewrite)

Theorem: cst-digit-conc-rep-of-tree-fix-cst

(defthm cst-digit-conc-rep-of-tree-fix-cst
  (equal (cst-digit-conc-rep (abnf::tree-fix abnf::cst))
         (cst-digit-conc-rep abnf::cst)))

Theorem: cst-digit-conc-rep-tree-equiv-congruence-on-cst

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

Function: cst-value-conc1-rep-elem

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

Theorem: treep-of-cst-value-conc1-rep-elem

(defthm treep-of-cst-value-conc1-rep-elem
  (b* ((abnf::cst1 (cst-value-conc1-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc1-rep-elem-match

(defthm cst-value-conc1-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 1))
           (b* ((abnf::cst1 (cst-value-conc1-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "false")))
  :rule-classes :rewrite)

Theorem: cst-value-conc1-rep-elem-of-tree-fix-cst

(defthm cst-value-conc1-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc1-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc1-rep-elem abnf::cst)))

Theorem: cst-value-conc1-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc1-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc1-rep-elem abnf::cst)
                  (cst-value-conc1-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-value-conc2-rep-elem

(defun cst-value-conc2-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 2))))
  (let ((__function__ 'cst-value-conc2-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-value-conc2-rep abnf::cst)))))

Theorem: treep-of-cst-value-conc2-rep-elem

(defthm treep-of-cst-value-conc2-rep-elem
  (b* ((abnf::cst1 (cst-value-conc2-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc2-rep-elem-match

(defthm cst-value-conc2-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 2))
           (b* ((abnf::cst1 (cst-value-conc2-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "null")))
  :rule-classes :rewrite)

Theorem: cst-value-conc2-rep-elem-of-tree-fix-cst

(defthm cst-value-conc2-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc2-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc2-rep-elem abnf::cst)))

Theorem: cst-value-conc2-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc2-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc2-rep-elem abnf::cst)
                  (cst-value-conc2-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-value-conc3-rep-elem

(defun cst-value-conc3-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 3))))
  (let ((__function__ 'cst-value-conc3-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-value-conc3-rep abnf::cst)))))

Theorem: treep-of-cst-value-conc3-rep-elem

(defthm treep-of-cst-value-conc3-rep-elem
  (b* ((abnf::cst1 (cst-value-conc3-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc3-rep-elem-match

(defthm cst-value-conc3-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 3))
           (b* ((abnf::cst1 (cst-value-conc3-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "true")))
  :rule-classes :rewrite)

Theorem: cst-value-conc3-rep-elem-of-tree-fix-cst

(defthm cst-value-conc3-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc3-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc3-rep-elem abnf::cst)))

Theorem: cst-value-conc3-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc3-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc3-rep-elem abnf::cst)
                  (cst-value-conc3-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-value-conc4-rep-elem

(defun cst-value-conc4-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 4))))
  (let ((__function__ 'cst-value-conc4-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-value-conc4-rep abnf::cst)))))

Theorem: treep-of-cst-value-conc4-rep-elem

(defthm treep-of-cst-value-conc4-rep-elem
  (b* ((abnf::cst1 (cst-value-conc4-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc4-rep-elem-match

(defthm cst-value-conc4-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 4))
           (b* ((abnf::cst1 (cst-value-conc4-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "object")))
  :rule-classes :rewrite)

Theorem: cst-value-conc4-rep-elem-of-tree-fix-cst

(defthm cst-value-conc4-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc4-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc4-rep-elem abnf::cst)))

Theorem: cst-value-conc4-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc4-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc4-rep-elem abnf::cst)
                  (cst-value-conc4-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-value-conc5-rep-elem

(defun cst-value-conc5-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 5))))
  (let ((__function__ 'cst-value-conc5-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-value-conc5-rep abnf::cst)))))

Theorem: treep-of-cst-value-conc5-rep-elem

(defthm treep-of-cst-value-conc5-rep-elem
  (b* ((abnf::cst1 (cst-value-conc5-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc5-rep-elem-match

(defthm cst-value-conc5-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 5))
           (b* ((abnf::cst1 (cst-value-conc5-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "array")))
  :rule-classes :rewrite)

Theorem: cst-value-conc5-rep-elem-of-tree-fix-cst

(defthm cst-value-conc5-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc5-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc5-rep-elem abnf::cst)))

Theorem: cst-value-conc5-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc5-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc5-rep-elem abnf::cst)
                  (cst-value-conc5-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-value-conc6-rep-elem

(defun cst-value-conc6-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 6))))
  (let ((__function__ 'cst-value-conc6-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-value-conc6-rep abnf::cst)))))

Theorem: treep-of-cst-value-conc6-rep-elem

(defthm treep-of-cst-value-conc6-rep-elem
  (b* ((abnf::cst1 (cst-value-conc6-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc6-rep-elem-match

(defthm cst-value-conc6-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 6))
           (b* ((abnf::cst1 (cst-value-conc6-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "number")))
  :rule-classes :rewrite)

Theorem: cst-value-conc6-rep-elem-of-tree-fix-cst

(defthm cst-value-conc6-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc6-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc6-rep-elem abnf::cst)))

Theorem: cst-value-conc6-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc6-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc6-rep-elem abnf::cst)
                  (cst-value-conc6-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-value-conc7-rep-elem

(defun cst-value-conc7-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare
       (xargs :guard (and (cst-matchp abnf::cst "value")
                          (equal (cst-value-conc? abnf::cst) 7))))
  (let ((__function__ 'cst-value-conc7-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-value-conc7-rep abnf::cst)))))

Theorem: treep-of-cst-value-conc7-rep-elem

(defthm treep-of-cst-value-conc7-rep-elem
  (b* ((abnf::cst1 (cst-value-conc7-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-value-conc7-rep-elem-match

(defthm cst-value-conc7-rep-elem-match
  (implies (and (cst-matchp abnf::cst "value")
                (equal (cst-value-conc? abnf::cst) 7))
           (b* ((abnf::cst1 (cst-value-conc7-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "string")))
  :rule-classes :rewrite)

Theorem: cst-value-conc7-rep-elem-of-tree-fix-cst

(defthm cst-value-conc7-rep-elem-of-tree-fix-cst
  (equal (cst-value-conc7-rep-elem (abnf::tree-fix abnf::cst))
         (cst-value-conc7-rep-elem abnf::cst)))

Theorem: cst-value-conc7-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-value-conc7-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-value-conc7-rep-elem abnf::cst)
                  (cst-value-conc7-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-false-conc-rep-elem

(defun cst-false-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "false")))
  (let ((__function__ 'cst-false-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-false-conc-rep abnf::cst)))))

Theorem: treep-of-cst-false-conc-rep-elem

(defthm treep-of-cst-false-conc-rep-elem
  (b* ((abnf::cst1 (cst-false-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-false-conc-rep-elem-match

(defthm cst-false-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "false")
           (b* ((abnf::cst1 (cst-false-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x66.61.6C.73.65")))
  :rule-classes :rewrite)

Theorem: cst-false-conc-rep-elem-of-tree-fix-cst

(defthm cst-false-conc-rep-elem-of-tree-fix-cst
  (equal (cst-false-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-false-conc-rep-elem abnf::cst)))

Theorem: cst-false-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-false-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-false-conc-rep-elem abnf::cst)
                  (cst-false-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-null-conc-rep-elem

(defun cst-null-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "null")))
  (let ((__function__ 'cst-null-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-null-conc-rep abnf::cst)))))

Theorem: treep-of-cst-null-conc-rep-elem

(defthm treep-of-cst-null-conc-rep-elem
  (b* ((abnf::cst1 (cst-null-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-null-conc-rep-elem-match

(defthm cst-null-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "null")
           (b* ((abnf::cst1 (cst-null-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x6E.75.6C.6C")))
  :rule-classes :rewrite)

Theorem: cst-null-conc-rep-elem-of-tree-fix-cst

(defthm cst-null-conc-rep-elem-of-tree-fix-cst
  (equal (cst-null-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-null-conc-rep-elem abnf::cst)))

Theorem: cst-null-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-null-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-null-conc-rep-elem abnf::cst)
                  (cst-null-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-true-conc-rep-elem

(defun cst-true-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "true")))
  (let ((__function__ 'cst-true-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-true-conc-rep abnf::cst)))))

Theorem: treep-of-cst-true-conc-rep-elem

(defthm treep-of-cst-true-conc-rep-elem
  (b* ((abnf::cst1 (cst-true-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-true-conc-rep-elem-match

(defthm cst-true-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "true")
           (b* ((abnf::cst1 (cst-true-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x74.72.75.65")))
  :rule-classes :rewrite)

Theorem: cst-true-conc-rep-elem-of-tree-fix-cst

(defthm cst-true-conc-rep-elem-of-tree-fix-cst
  (equal (cst-true-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-true-conc-rep-elem abnf::cst)))

Theorem: cst-true-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-true-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-true-conc-rep-elem abnf::cst)
                  (cst-true-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-decimal-point-conc-rep-elem

(defun cst-decimal-point-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "decimal-point")))
  (let ((__function__ 'cst-decimal-point-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (cst-decimal-point-conc-rep abnf::cst)))))

Theorem: treep-of-cst-decimal-point-conc-rep-elem

(defthm treep-of-cst-decimal-point-conc-rep-elem
  (b* ((abnf::cst1 (cst-decimal-point-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-decimal-point-conc-rep-elem-match

(defthm cst-decimal-point-conc-rep-elem-match
 (implies
      (cst-matchp abnf::cst "decimal-point")
      (b* ((abnf::cst1 (cst-decimal-point-conc-rep-elem abnf::cst)))
        (cst-matchp abnf::cst1 "%x2E")))
 :rule-classes :rewrite)

Theorem: cst-decimal-point-conc-rep-elem-of-tree-fix-cst

(defthm cst-decimal-point-conc-rep-elem-of-tree-fix-cst
 (equal (cst-decimal-point-conc-rep-elem (abnf::tree-fix abnf::cst))
        (cst-decimal-point-conc-rep-elem abnf::cst)))

Theorem: cst-decimal-point-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-decimal-point-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-decimal-point-conc-rep-elem abnf::cst)
                  (cst-decimal-point-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-digit1-9-conc-rep-elem

(defun cst-digit1-9-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "digit1-9")))
  (let ((__function__ 'cst-digit1-9-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-digit1-9-conc-rep abnf::cst)))))

Theorem: treep-of-cst-digit1-9-conc-rep-elem

(defthm treep-of-cst-digit1-9-conc-rep-elem
  (b* ((abnf::cst1 (cst-digit1-9-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-digit1-9-conc-rep-elem-match

(defthm cst-digit1-9-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "digit1-9")
           (b* ((abnf::cst1 (cst-digit1-9-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x31-39")))
  :rule-classes :rewrite)

Theorem: cst-digit1-9-conc-rep-elem-of-tree-fix-cst

(defthm cst-digit1-9-conc-rep-elem-of-tree-fix-cst
  (equal (cst-digit1-9-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-digit1-9-conc-rep-elem abnf::cst)))

Theorem: cst-digit1-9-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-digit1-9-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-digit1-9-conc-rep-elem abnf::cst)
                  (cst-digit1-9-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-minus-conc-rep-elem

(defun cst-minus-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "minus")))
  (let ((__function__ 'cst-minus-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-minus-conc-rep abnf::cst)))))

Theorem: treep-of-cst-minus-conc-rep-elem

(defthm treep-of-cst-minus-conc-rep-elem
  (b* ((abnf::cst1 (cst-minus-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-minus-conc-rep-elem-match

(defthm cst-minus-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "minus")
           (b* ((abnf::cst1 (cst-minus-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x2D")))
  :rule-classes :rewrite)

Theorem: cst-minus-conc-rep-elem-of-tree-fix-cst

(defthm cst-minus-conc-rep-elem-of-tree-fix-cst
  (equal (cst-minus-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-minus-conc-rep-elem abnf::cst)))

Theorem: cst-minus-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-minus-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-minus-conc-rep-elem abnf::cst)
                  (cst-minus-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-plus-conc-rep-elem

(defun cst-plus-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "plus")))
  (let ((__function__ 'cst-plus-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-plus-conc-rep abnf::cst)))))

Theorem: treep-of-cst-plus-conc-rep-elem

(defthm treep-of-cst-plus-conc-rep-elem
  (b* ((abnf::cst1 (cst-plus-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-plus-conc-rep-elem-match

(defthm cst-plus-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "plus")
           (b* ((abnf::cst1 (cst-plus-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x2B")))
  :rule-classes :rewrite)

Theorem: cst-plus-conc-rep-elem-of-tree-fix-cst

(defthm cst-plus-conc-rep-elem-of-tree-fix-cst
  (equal (cst-plus-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-plus-conc-rep-elem abnf::cst)))

Theorem: cst-plus-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-plus-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-plus-conc-rep-elem abnf::cst)
                  (cst-plus-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-zero-conc-rep-elem

(defun cst-zero-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "zero")))
  (let ((__function__ 'cst-zero-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-zero-conc-rep abnf::cst)))))

Theorem: treep-of-cst-zero-conc-rep-elem

(defthm treep-of-cst-zero-conc-rep-elem
  (b* ((abnf::cst1 (cst-zero-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-zero-conc-rep-elem-match

(defthm cst-zero-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "zero")
           (b* ((abnf::cst1 (cst-zero-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x30")))
  :rule-classes :rewrite)

Theorem: cst-zero-conc-rep-elem-of-tree-fix-cst

(defthm cst-zero-conc-rep-elem-of-tree-fix-cst
  (equal (cst-zero-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-zero-conc-rep-elem abnf::cst)))

Theorem: cst-zero-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-zero-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-zero-conc-rep-elem abnf::cst)
                  (cst-zero-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-escape-conc-rep-elem

(defun cst-escape-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "escape")))
  (let ((__function__ 'cst-escape-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-escape-conc-rep abnf::cst)))))

Theorem: treep-of-cst-escape-conc-rep-elem

(defthm treep-of-cst-escape-conc-rep-elem
  (b* ((abnf::cst1 (cst-escape-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-escape-conc-rep-elem-match

(defthm cst-escape-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "escape")
           (b* ((abnf::cst1 (cst-escape-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x5C")))
  :rule-classes :rewrite)

Theorem: cst-escape-conc-rep-elem-of-tree-fix-cst

(defthm cst-escape-conc-rep-elem-of-tree-fix-cst
  (equal (cst-escape-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-escape-conc-rep-elem abnf::cst)))

Theorem: cst-escape-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-escape-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-escape-conc-rep-elem abnf::cst)
                  (cst-escape-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-quotation-mark-conc-rep-elem

(defun cst-quotation-mark-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "quotation-mark")))
  (let ((__function__ 'cst-quotation-mark-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0
                         (cst-quotation-mark-conc-rep abnf::cst)))))

Theorem: treep-of-cst-quotation-mark-conc-rep-elem

(defthm treep-of-cst-quotation-mark-conc-rep-elem
  (b* ((abnf::cst1 (cst-quotation-mark-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-quotation-mark-conc-rep-elem-match

(defthm cst-quotation-mark-conc-rep-elem-match
 (implies
     (cst-matchp abnf::cst "quotation-mark")
     (b* ((abnf::cst1 (cst-quotation-mark-conc-rep-elem abnf::cst)))
       (cst-matchp abnf::cst1 "%x22")))
 :rule-classes :rewrite)

Theorem: cst-quotation-mark-conc-rep-elem-of-tree-fix-cst

(defthm cst-quotation-mark-conc-rep-elem-of-tree-fix-cst
  (equal
       (cst-quotation-mark-conc-rep-elem (abnf::tree-fix abnf::cst))
       (cst-quotation-mark-conc-rep-elem abnf::cst)))

Theorem: cst-quotation-mark-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm
      cst-quotation-mark-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-quotation-mark-conc-rep-elem abnf::cst)
                  (cst-quotation-mark-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

Function: cst-digit-conc-rep-elem

(defun cst-digit-conc-rep-elem (abnf::cst)
  (declare (xargs :guard (abnf::treep abnf::cst)))
  (declare (xargs :guard (cst-matchp abnf::cst "digit")))
  (let ((__function__ 'cst-digit-conc-rep-elem))
    (declare (ignorable __function__))
    (abnf::tree-fix (nth 0 (cst-digit-conc-rep abnf::cst)))))

Theorem: treep-of-cst-digit-conc-rep-elem

(defthm treep-of-cst-digit-conc-rep-elem
  (b* ((abnf::cst1 (cst-digit-conc-rep-elem abnf::cst)))
    (abnf::treep abnf::cst1))
  :rule-classes :rewrite)

Theorem: cst-digit-conc-rep-elem-match

(defthm cst-digit-conc-rep-elem-match
  (implies (cst-matchp abnf::cst "digit")
           (b* ((abnf::cst1 (cst-digit-conc-rep-elem abnf::cst)))
             (cst-matchp abnf::cst1 "%x30-39")))
  :rule-classes :rewrite)

Theorem: cst-digit-conc-rep-elem-of-tree-fix-cst

(defthm cst-digit-conc-rep-elem-of-tree-fix-cst
  (equal (cst-digit-conc-rep-elem (abnf::tree-fix abnf::cst))
         (cst-digit-conc-rep-elem abnf::cst)))

Theorem: cst-digit-conc-rep-elem-tree-equiv-congruence-on-cst

(defthm cst-digit-conc-rep-elem-tree-equiv-congruence-on-cst
  (implies (abnf::tree-equiv abnf::cst cst-equiv)
           (equal (cst-digit-conc-rep-elem abnf::cst)
                  (cst-digit-conc-rep-elem cst-equiv)))
  :rule-classes :congruence)

*all-grammar-rules*-tree-operations

Definitions and Theorems

all-grammar-rules-tree-operations