• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
            • Dynamic-semantics
            • Concrete-syntax
              • Lexer
              • Parser
              • Grammar-old
              • Grammar
                • Cst-literal-conc?
                • Cst-token-conc?
                  • Cst-expression-conc?
                  • Cst-list-list-conc-matchp$
                  • Cst-lexeme-conc?
                  • Cst-list-list-alt-matchp$
                  • Cst-identifier-rest-conc?
                  • Cst-list-rep-matchp$
                  • Cst-list-elem-matchp$
                  • Cst-comment-conc?
                  • Abnf-tree-wrap-fn
                  • Abnf-tree-with-root-p
                  • Cst-nonzero-decimal-digit-conc-rep-elem
                  • Cst-matchp$
                  • Abnf-tree-wrap
                  • Cst-nonzero-decimal-digit-conc-rep
                  • Cst-identifier-rest-conc2-rep-elem
                  • Cst-identifier-rest-conc2-rep
                  • Cst-identifier-rest-conc1-rep-elem
                  • Cst-identifier-rest-conc1-rep
                  • Cst-expression-conc3-rep-elem
                  • Cst-expression-conc2-rep-elem
                  • Cst-uppercase-letter-conc-rep-elem
                  • Cst-uppercase-letter-conc-rep
                  • Cst-switch-statement-conc
                  • Cst-nonzero-decimal-digit-conc
                  • Cst-lowercase-letter-conc-rep-elem
                  • Cst-lowercase-letter-conc-rep
                  • Cst-literal-conc5-rep-elem
                  • Cst-literal-conc4-rep-elem
                  • Cst-literal-conc3-rep-elem
                  • Cst-literal-conc2-rep-elem
                  • Cst-literal-conc1-rep-elem
                  • Cst-lexeme-conc3-rep-elem
                  • Cst-lexeme-conc2-rep-elem
                  • Cst-lexeme-conc1-rep-elem
                  • Cst-identifier-rest-conc2
                  • Cst-identifier-rest-conc1
                  • Cst-function-definition-conc
                  • Cst-expression-conc3-rep
                  • Cst-expression-conc2-rep
                  • Cst-expression-conc1-rep-elem
                  • Cst-expression-conc1-rep
                  • Cst-end-of-line-comment-conc
                  • Cst-decimal-digit-conc-rep-elem
                  • Cst-comment-conc2-rep-elem
                  • Cst-comment-conc1-rep-elem
                  • Cst-uppercase-letter-conc
                  • Cst-token-conc4-rep-elem
                  • Cst-token-conc3-rep-elem
                  • Cst-token-conc2-rep-elem
                  • Cst-token-conc1-rep-elem
                  • Cst-lowercase-letter-conc
                  • Cst-literal-conc5-rep
                  • Cst-literal-conc5
                  • Cst-literal-conc4-rep
                  • Cst-literal-conc4
                  • Cst-literal-conc3-rep
                  • Cst-literal-conc3
                  • Cst-literal-conc2-rep
                  • Cst-literal-conc2
                  • Cst-literal-conc1-rep
                  • Cst-literal-conc1
                  • Cst-lexeme-conc3-rep
                  • Cst-lexeme-conc2-rep
                  • Cst-lexeme-conc1-rep
                  • Cst-if-statement-conc
                  • Cst-function-call-conc
                  • Cst-for-statement-conc
                  • Cst-expression-conc3
                  • Cst-expression-conc2
                  • Cst-expression-conc1
                  • Cst-escape-sequence-conc
                  • Cst-decimal-digit-conc-rep
                  • Cst-decimal-digit-conc
                  • Cst-comment-conc2-rep
                  • Cst-comment-conc2
                  • Cst-comment-conc1-rep
                  • Cst-comment-conc1
                  • Cst-block-comment-conc
                  • Cst-whitespace-conc
                  • Cst-token-conc4-rep
                  • Cst-token-conc4
                  • Cst-token-conc3-rep
                  • Cst-token-conc3
                  • Cst-token-conc2-rep
                  • Cst-token-conc2
                  • Cst-token-conc1-rep
                  • Cst-token-conc1
                  • Cst-squote-conc-rep-elem
                  • Cst-squote-conc-rep
                  • Cst-lexeme-conc3
                  • Cst-lexeme-conc2
                  • Cst-lexeme-conc1
                  • Cst-identifier-conc
                  • Cst-hex-string-conc
                  • Cst-hex-number-conc
                  • Cst-dquote-conc-rep-elem
                  • Cst-dquote-conc-rep
                  • *grammar*
                  • Cst-squote-conc
                  • Cst-path-conc
                  • Cst-lf-conc-rep-elem
                  • Cst-lf-conc-rep
                  • Cst-dquote-conc
                  • Cst-cr-conc-rep-elem
                  • Cst-cr-conc-rep
                  • Cst-block-conc
                  • Abnf-tree-list-with-root-p
                  • Cst-lf-conc
                  • Cst-cr-conc
                  • Cst-%xe-7f-nat
                  • Cst-%xb-c-nat
                  • Cst-%x61-7a-nat
                  • Cst-%x5d-7e-nat
                  • Cst-%x41-5a-nat
                  • Cst-%x31-39-nat
                  • Cst-%x30-7f-nat
                  • Cst-%x30-39-nat
                  • Cst-%x2b-7f-nat
                  • Cst-%x2b-2e-nat
                  • Cst-%x28-5b-nat
                  • Cst-%x23-5b-nat
                  • Cst-%x20-26-nat
                  • Cst-%x20-21-nat
                  • Cst-%x0-9-nat
                  • Cst-%x0-29-nat
                • Tokenizer
              • Static-soundness
              • Static-semantics
              • Errors
            • Yul-json
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Grammar

    Cst-token-conc?

    Signature
    (cst-token-conc? abnf::cst) → number
    Arguments
    abnf::cst — Guard (abnf::treep abnf::cst).
    Returns
    number — Type (posp number).

    Definitions and Theorems

    Function: cst-token-conc?

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

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

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

    Theorem: cst-token-conc?-possibilities

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

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

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

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

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

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

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

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

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

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

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

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

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