• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Tree-utilities
      • Notation
      • Grammar-parser
        • Grammar-parser-implementation
        • Grammar-parser-correctness
          • Grammar-parser-completeness
          • Grammar-parser-soundness
            • Grammar-parser-tree-matching
            • Grammar-parser-input-decomposition
              • Input-decomposition-of-parse-alt/conc/rep/elem/group/option
              • Input-decomposition-of-parse-case-insensitive-string
              • Input-decomposition-of-parse-*wsp/vchar
              • Input-decomposition-of-parse-*digit-star-*digit
              • Input-decomposition-of-parse-*cwsp-cnl
              • Input-decomposition-of-parse-*-rule-/-*cwsp-cnl
              • Input-decomposition-of-parse-*-in-either-range
              • Input-decomposition-of-parse-*-dot-1*hexdig
              • Input-decomposition-of-parse-*-dot-1*digit
              • Input-decomposition-of-parse-*-dot-1*bit
              • Input-decomposition-of-parse-*-alpha/digit/dash
              • Input-decomposition-of-parse-wsp/vchar
              • Input-decomposition-of-parse-rulename
              • Input-decomposition-of-parse-rulelist
              • Input-decomposition-of-parse-rule-/-*cwsp-cnl
              • Input-decomposition-of-parse-quoted-string
              • Input-decomposition-of-parse-prose-val
              • Input-decomposition-of-parse-num-val
              • Input-decomposition-of-parse-in-range
              • Input-decomposition-of-parse-in-either-range
              • Input-decomposition-of-parse-ichar2
              • Input-decomposition-of-parse-hex-val-rest
              • Input-decomposition-of-parse-hex-val
              • Input-decomposition-of-parse-equal-/-equal-slash
              • Input-decomposition-of-parse-elements
              • Input-decomposition-of-parse-dot-1*hexdig
              • Input-decomposition-of-parse-dot-1*digit
              • Input-decomposition-of-parse-dot-1*bit
              • Input-decomposition-of-parse-defined-as
              • Input-decomposition-of-parse-dec-val-rest
              • Input-decomposition-of-parse-dec-val
              • Input-decomposition-of-parse-dash-1*hexdig
              • Input-decomposition-of-parse-dash-1*digit
              • Input-decomposition-of-parse-dash-1*bit
              • Input-decomposition-of-parse-comment
              • Input-decomposition-of-parse-cnl-wsp
              • Input-decomposition-of-parse-char-val
              • Input-decomposition-of-parse-case-sensitive-string
              • Input-decomposition-of-parse-bin/dec/hex-val
              • Input-decomposition-of-parse-bin-val-rest
              • Input-decomposition-of-parse-bin-val
              • Input-decomposition-of-parse-alpha/digit/dash
              • Input-decomposition-of-parse-1*hexdig
              • Input-decomposition-of-parse-1*digit
              • Input-decomposition-of-parse-1*cwsp
              • Input-decomposition-of-parse-1*bit
              • Input-decomposition-of-parse-1*-dot-1*hexdig
              • Input-decomposition-of-parse-1*-dot-1*digit
              • Input-decomposition-of-parse-1*-dot-1*bit
              • Input-decomposition-of-parse-?%i
              • Input-decomposition-of-parse-?repeat
              • Input-decomposition-of-parse-*hexdig
              • Input-decomposition-of-parse-*digit
              • Input-decomposition-of-parse-*cwsp
              • Input-decomposition-of-parse-*bit
              • Input-decomposition-of-parse-wsp
              • Input-decomposition-of-parse-vchar
              • Input-decomposition-of-parse-sp
              • Input-decomposition-of-parse-rule
              • Input-decomposition-of-parse-repeat
              • Input-decomposition-of-parse-lf
              • Input-decomposition-of-parse-ichar
              • Input-decomposition-of-parse-htab
              • Input-decomposition-of-parse-hexdig
              • Input-decomposition-of-parse-exact
              • Input-decomposition-of-parse-dquote
              • Input-decomposition-of-parse-digit
              • Input-decomposition-of-parse-cwsp
              • Input-decomposition-of-parse-crlf
              • Input-decomposition-of-parse-cr
              • Input-decomposition-of-parse-cnl
              • Input-decomposition-of-parse-bit
              • Input-decomposition-of-parse-any
              • Input-decomposition-of-parse-alpha
            • Parse-treep-of-parse-grammar
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
      • Differences-with-paper
      • Constructor-utilities
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Grammar-parser-input-decomposition

Input-decomposition-of-parse-*digit

Input decomposition theorem for parse-*digit.

Definitions and Theorems

Theorem: input-decomposition-of-parse-*digit

(defthm input-decomposition-of-parse-*digit
  (b* (((mv & trees rest-input)
        (parse-*digit input)))
    (equal (append (tree-list->string trees)
                   rest-input)
           (nat-list-fix input))))