• 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-disambiguation
            • Grammar-parser-constraints-from-tree-matching
            • Grammar-parser-constraints-from-parsing
            • Grammar-parser-disambiguating-restrictions
            • Grammar-parser-parsing-failure-propagation
            • Parse-alt/conc/rep/elem/group/option-when-tree-/-tree-list-match-lemmas
            • Parse-grammar-when-tree-match
            • Parse-*-in-either-range-when-tree-list-match
            • Parse-in-either-range-when-tree-match
            • Parse-element-when-tree-match-induction-step-1+2+3+4+5
            • Pred-concatenation
            • Pred-conc-rest
            • Pred-alternation
            • Pred-alt-rest
            • Pred-conc-rest-comp
            • Pred-alt-rest-comp
            • Parse-elements-when-tree-match
            • Pred-repetition
            • Pred-element
            • Parse-*-rule-/-*cwsp-cnl-when-tree-list-match-and-restriction
            • Parse-option-when-tree-match-induction-step-3
            • Parse-option-when-tree-match-induction-step-2
            • Parse-option-when-tree-match-induction-step-1+2+3
            • Parse-group-when-tree-match-induction-step-3
            • Parse-group-when-tree-match-induction-step-2
            • Parse-group-when-tree-match-induction-step-1+2+3
            • Parse-bin/dec/hex-val-when-tree-match
            • Parse-alt-rest-when-tree-list-match
            • Parse-alt-rest-comp-when-tree-match-induction-step-2
            • Parse-alt-rest-comp-when-tree-match-induction-step-1
            • Parse-*bit-when-tree-list-match
            • Parse-*-dot-1*bit-when-tree-list-match
            • Parse-rulelist-when-tree-match-and-restriction
            • Parse-exact-when-tree-match
            • Parse-element-when-tree-match-induction-step-3
            • Parse-element-when-tree-match-induction-step-2
            • Parse-element-when-tree-match-induction-step-1
            • Parse-conc-rest-when-tree-list-match
            • Parse-conc-rest-comp-when-tree-match-induction-step-2
            • Parse-conc-rest-comp-when-tree-match-induction-step-1+2
            • Parse-conc-rest-comp-when-tree-match-induction-step-1
            • Parse-bin-val-rest-when-tree-match
            • Parse-alternation-when-tree-match
            • Parse-alt-rest-comp-when-tree-match-induction-step-1+2
            • Parse-alt-rest-comp-when-tree-match
            • Parse-1*-dot-1*bit-when-tree-list-match
            • Pred-option
            • Pred-group
            • Parse-?%i-when-tree-match
            • Parse-*digit-when-tree-list-match
            • Parse-*cwsp-when-tree-list-match
            • Parse-wsp-when-tree-match
            • Parse-repetition-when-tree-match-induction-step-2
            • Parse-repetition-when-tree-match-induction-step-1+2
            • Parse-repetition-when-tree-match-induction-step-1
            • Parse-repetition-when-tree-match
            • Parse-option-when-tree-match-induction-step-1
            • Parse-ichar-when-tree-match
            • Parse-htab-when-tree-match
            • Parse-hex-val-when-tree-match
            • Parse-group-when-tree-match-induction-step-1
            • Parse-equal-/-equal-slash-when-tree-match
            • Parse-element-when-tree-match-induction-step-5
            • Parse-element-when-tree-match-induction-step-4
            • Parse-element-when-tree-match
            • Parse-dot-1*bit-when-tree-match
            • Parse-dec-val-when-tree-match
            • Parse-cr-when-tree-match
            • Parse-concatenation-when-tree-match-induction-step-2
            • Parse-concatenation-when-tree-match
            • Parse-conc-rest-comp-when-tree-match
            • Parse-cnl-when-tree-match
            • Parse-bin-val-when-tree-match
            • Parse-alternation-when-tree-match-induction-step-2
            • Parse-alpha-when-tree-match
            • Parse-1*cwsp-when-tree-list-match
            • Parse-1*bit-when-tree-list-match
            • Parse-*wsp/vchar-when-tree-list-match
            • Parse-*hexdig-when-tree-list-match
            • Parse-*digit-star-*digit-when-tree-match
            • Parse-*cwsp-cnl-when-tree-match
            • Parse-*-dot-1*hexdig-when-tree-list-match
            • Parse-*-dot-1*digit-when-tree-list-match
            • Parse-*-alpha/digit/dash-when-tree-list-match
            • Parse-sp-when-tree-match
            • Parse-rule-/-*cwsp-cnl-when-tree-match
            • Parse-rule-when-tree-match
            • Parse-num-val-when-tree-match
            • Parse-lf-when-tree-match
            • Parse-in-range-when-tree-match
            • Parse-ichar2-when-tree-match
            • Parse-hex-val-rest-when-tree-match
            • Parse-defined-as-when-tree-match
            • Parse-dec-val-rest-when-tree-match
            • Parse-crlf-when-tree-match
            • Parse-conc-rest-when-tree-list-match-induction-step-2
            • Parse-case-sensitive-string-when-tree-match
            • Parse-case-insensitive-string-when-tree-match
            • Parse-bit-when-tree-match
            • Parse-alt-rest-when-tree-list-match-induction-step-2
            • Parse-1*hexdig-when-tree-list-match
            • Parse-1*digit-when-tree-list-match
            • Parse-1*-dot-1*hexdig-when-tree-list-match
            • Parse-1*-dot-1*digit-when-tree-list-match
            • Parse-?repeat-when-tree-match
            • Parse-wsp/vchar-when-tree-match
            • Parse-vchar-when-tree-match
            • Parse-rulename-when-tree-match
            • Parse-repeat-when-tree-match
            • Parse-quoted-string-when-tree-match
            • Parse-prose-val-when-tree-match
            • Parse-option-when-tree-match
            • Parse-hexdig-when-tree-match
            • Parse-group-when-tree-match
            • Parse-element-when-tree-match-induction-step-6
            • Parse-element-when-tree-match-base-case
            • Parse-dquote-when-tree-match
            • Parse-dot-1*hexdig-when-tree-match
            • Parse-dot-1*digit-when-tree-match
            • Parse-digit-when-tree-match
            • Parse-dash-1*hexdig-when-tree-match
            • Parse-dash-1*digit-when-tree-match
            • Parse-dash-1*bit-when-tree-match
            • Parse-cwsp-when-tree-match
            • Parse-concatenation-when-tree-match-induction-step-1
            • Parse-conc-rest-when-tree-list-match-induction-step-1
            • Parse-conc-rest-comp-when-tree-match-base-case
            • Parse-comment-when-tree-match
            • Parse-cnl-wsp-when-tree-match
            • Parse-char-val-when-tree-match
            • Parse-alternation-when-tree-match-induction-step-1
            • Parse-alt-rest-when-tree-list-match-induction-step-1
            • Parse-alt-rest-comp-when-tree-match-base-case
            • Parse-alpha/digit/dash-when-tree-match
            • Parse-option-when-tree-match-base-case
            • Parse-group-when-tree-match-base-case
            • Parse-any-of-cons
          • Grammar-parser-soundness
      • 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-completeness

Parse-in-either-range-when-tree-match

Completeness theorem for parse-in-either-range.

Definitions and Theorems

Theorem: parse-in-either-range-when-tree-match

(defthm parse-in-either-range-when-tree-match
 (implies
  (and
   (tree-match-element-p tree element *grammar*)
   (element-case element :group)
   (b* ((alternation (element-group->get element)))
    (and
     (consp alternation)
     (consp (cdr alternation))
     (atom (cddr alternation))
     (b* ((concatenation1 (car alternation))
          (concatenation2 (cadr alternation)))
      (and
       (consp concatenation1)
       (atom (cdr concatenation1))
       (consp concatenation2)
       (atom (cdr concatenation2))
       (b* ((repetition1 (car concatenation1))
            (repetition2 (car concatenation2)))
        (and
         (equal (repetition->range repetition1)
                (make-repeat-range :min 1
                                   :max (nati-finite 1)))
         (equal (repetition->range repetition2)
                (make-repeat-range :min 1
                                   :max (nati-finite 1)))
         (b* ((element1 (repetition->element repetition1))
              (element2 (repetition->element repetition2)))
          (and
           (element-case element1 :num-val)
           (num-val-case (element-num-val->get element1)
                         :range)
           (equal
                (num-val-range->min (element-num-val->get element1))
                min1)
           (equal
                (num-val-range->max (element-num-val->get element1))
                max1)
           (element-case element2 :num-val)
           (num-val-case (element-num-val->get element2)
                         :range)
           (equal
                (num-val-range->min (element-num-val->get element2))
                min2)
           (equal
                (num-val-range->max (element-num-val->get element2))
                max2)))))))))
   (< max1 min2))
  (equal
     (parse-in-either-range min1 max1 min2 max2
                            (append (tree->string tree) rest-input))
     (mv nil (tree-fix tree)
         (nat-list-fix rest-input)))))