• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Tree-utilities
        • Check-tree-nonleaf-num-range-4
        • Check-tree-nonleaf-num-range-3
        • Check-tree-num-range-4
        • Check-tree-nonleaf-num-range-2
        • Check-tree-num-range-3
        • Check-tree-num-range-2
        • Tree-list-tuple10
        • Check-tree-nonleaf-num-range
        • Tree-list-tuple9
        • Tree-list-tuple8
        • Tree-list-tuple7
        • Tree-list-tuple6
        • Check-tree-nonleaf-num-seq
        • Check-tree-num-range
        • Tree-list-tuple5
        • Check-tree-nonleaf-10
        • Check-tree-nonleaf-9
        • Check-tree-nonleaf-8
        • Check-tree-nonleaf-7
        • Check-tree-list-list-10
        • Tree-list-tuple4
        • Check-tree-nonleaf-6
        • Check-tree-nonleaf-5
        • Check-tree-list-list-9
        • Check-tree-nonleaf-4
        • Check-tree-nonleaf-3
        • Check-tree-nonleaf-2
        • Check-tree-nonleaf
        • Check-tree-list-list-8
        • Check-tree-nonleaf-1-1
        • Check-tree-nonleaf-1
        • Check-tree-list-list-7
        • Tree-list-tuple3
        • Pass
        • Check-tree-list-list-6
        • Check-tree-list-list-5
        • Tree=>string
        • Tree-list-tuple2
        • Check-tree-list-list-4
        • Check-tree-list-list-3
        • Check-tree-ichars
        • Check-tree-schars
        • Check-tree-num-seq
        • Check-tree-list-list-2
        • Tree-list-tuple9-result
        • Tree-list-tuple8-result
        • Tree-list-tuple7-result
        • Tree-list-tuple6-result
        • Tree-list-tuple5-result
        • Tree-list-tuple4-result
        • Tree-list-tuple3-result
        • Tree-list-tuple2-result
        • Tree-list-tuple10-result
        • Pass-result
        • Check-tree-list-list-1
        • Tree-info-for-error
        • Check-tree-list-1
        • Check-tree-nonleaf?
        • Check-tree-leafterm
      • Notation
      • Grammar-parser
      • 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

• Tree-utilities

Check-tree-nonleaf-num-range-4

Check if an ABNF tree is a non-leaf tree with a given optional rule name or no rule name as root and a list of one list of one subtree, where the subtree is a leaf tree with a single natural number in one of four given ranges, returning that natural number if successful.

Signature

(check-tree-nonleaf-num-range-4 
     tree rulename? 
     min1 max1 min2 max2 min3 max3 min4 max4) 
 
  → 
nat

Arguments

tree — Guard (treep tree).

rulename? — Guard (acl2::maybe-stringp rulename?).

min1 — Guard (natp min1).

max1 — Guard (natp max1).

min2 — Guard (natp min2).

max2 — Guard (natp max2).

min3 — Guard (natp min3).

max3 — Guard (natp max3).

min4 — Guard (natp min4).

max4 — Guard (natp max4).

Returns

nat — Type (nat-resultp nat).

Definitions and Theorems

Function: check-tree-nonleaf-num-range-4

(defun check-tree-nonleaf-num-range-4
       (tree rulename?
             min1 max1 min2 max2 min3 max3 min4 max4)
  (declare (xargs :guard (and (treep tree)
                              (acl2::maybe-stringp rulename?)
                              (natp min1)
                              (natp max1)
                              (natp min2)
                              (natp max2)
                              (natp min3)
                              (natp max3)
                              (natp min4)
                              (natp max4))))
  (let ((__function__ 'check-tree-nonleaf-num-range-4))
    (declare (ignorable __function__))
    (b* (((okf tree)
          (check-tree-nonleaf-1-1 tree rulename?)))
      (check-tree-num-range-4 tree min1
                              max1 min2 max2 min3 max3 min4 max4))))

Theorem: nat-resultp-of-check-tree-nonleaf-num-range-4

(defthm nat-resultp-of-check-tree-nonleaf-num-range-4
  (b* ((nat (check-tree-nonleaf-num-range-4
                 tree rulename? min1
                 max1 min2 max2 min3 max3 min4 max4)))
    (nat-resultp nat))
  :rule-classes :rewrite)

Theorem: natp-of-check-tree-nonleaf-num-range-4

(defthm natp-of-check-tree-nonleaf-num-range-4
  (b* ((acl2::?nat (check-tree-nonleaf-num-range-4
                        tree rulename? min1
                        max1 min2 max2 min3 max3 min4 max4)))
    (implies (not (reserrp nat))
             (natp nat)))
  :rule-classes :forward-chaining)

Theorem: check-tree-nonleaf-num-range-4-bounds

(defthm check-tree-nonleaf-num-range-4-bounds
  (b* ((acl2::?nat (check-tree-nonleaf-num-range-4
                        tree rulename? min1
                        max1 min2 max2 min3 max3 min4 max4)))
    (implies (not (reserrp nat))
             (or (and (<= (nfix min1) nat)
                      (<= nat (nfix max1)))
                 (and (<= (nfix min2) nat)
                      (<= nat (nfix max2)))
                 (and (<= (nfix min3) nat)
                      (<= nat (nfix max3)))
                 (and (<= (nfix min4) nat)
                      (<= nat (nfix max4))))))
  :rule-classes nil)

Theorem: check-tree-nonleaf-num-range-4-of-tree-fix-tree

(defthm check-tree-nonleaf-num-range-4-of-tree-fix-tree
  (equal (check-tree-nonleaf-num-range-4
              (tree-fix tree)
              rulename?
              min1 max1 min2 max2 min3 max3 min4 max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-tree-equiv-congruence-on-tree

(defthm check-tree-nonleaf-num-range-4-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree-equiv rulename? min1
                       max1 min2 max2 min3 max3 min4 max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-maybe-string-fix-rulename?

(defthm check-tree-nonleaf-num-range-4-of-maybe-string-fix-rulename?
  (equal (check-tree-nonleaf-num-range-4
              tree (acl2::maybe-string-fix rulename?)
              min1 max1 min2 max2 min3 max3 min4 max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-maybe-string-equiv-congruence-on-rulename?

(defthm
 check-tree-nonleaf-num-range-4-maybe-string-equiv-congruence-on-rulename?
 (implies (acl2::maybe-string-equiv rulename? rulename?-equiv)
          (equal (check-tree-nonleaf-num-range-4
                      tree rulename?
                      min1 max1 min2 max2 min3 max3 min4 max4)
                 (check-tree-nonleaf-num-range-4
                      tree rulename?-equiv min1
                      max1 min2 max2 min3 max3 min4 max4)))
 :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-min1

(defthm check-tree-nonleaf-num-range-4-of-nfix-min1
  (equal (check-tree-nonleaf-num-range-4
              tree rulename? (nfix min1)
              max1 min2 max2 min3 max3 min4 max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min1

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min1
  (implies (acl2::nat-equiv min1 min1-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1-equiv
                       max1 min2 max2 min3 max3 min4 max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-max1

(defthm check-tree-nonleaf-num-range-4-of-nfix-max1
 (equal
     (check-tree-nonleaf-num-range-4 tree rulename? min1 (nfix max1)
                                     min2 max2 min3 max3 min4 max4)
     (check-tree-nonleaf-num-range-4
          tree rulename? min1
          max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max1

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max1
 (implies
  (acl2::nat-equiv max1 max1-equiv)
  (equal
    (check-tree-nonleaf-num-range-4
         tree rulename?
         min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-nonleaf-num-range-4 tree rulename? min1 max1-equiv
                                    min2 max2 min3 max3 min4 max4)))
 :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-min2

(defthm check-tree-nonleaf-num-range-4-of-nfix-min2
  (equal (check-tree-nonleaf-num-range-4
              tree rulename? min1 max1 (nfix min2)
              max2 min3 max3 min4 max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min2

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min2
  (implies (acl2::nat-equiv min2 min2-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1 max1
                       min2-equiv max2 min3 max3 min4 max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-max2

(defthm check-tree-nonleaf-num-range-4-of-nfix-max2
  (equal (check-tree-nonleaf-num-range-4
              tree
              rulename? min1 max1 min2 (nfix max2)
              min3 max3 min4 max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max2

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max2
  (implies (acl2::nat-equiv max2 max2-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1 max1
                       min2 max2-equiv min3 max3 min4 max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-min3

(defthm check-tree-nonleaf-num-range-4-of-nfix-min3
 (equal
     (check-tree-nonleaf-num-range-4 tree rulename?
                                     min1 max1 min2 max2 (nfix min3)
                                     max3 min4 max4)
     (check-tree-nonleaf-num-range-4
          tree rulename? min1
          max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min3

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min3
  (implies (acl2::nat-equiv min3 min3-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1 max1
                       min2 max2 min3-equiv max3 min4 max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-max3

(defthm check-tree-nonleaf-num-range-4-of-nfix-max3
  (equal (check-tree-nonleaf-num-range-4
              tree rulename?
              min1 max1 min2 max2 min3 (nfix max3)
              min4 max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max3

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max3
  (implies (acl2::nat-equiv max3 max3-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1 max1
                       min2 max2 min3 max3-equiv min4 max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-min4

(defthm check-tree-nonleaf-num-range-4-of-nfix-min4
  (equal (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 (nfix min4)
              max4)
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min4

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-min4
  (implies (acl2::nat-equiv min4 min4-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1 max1
                       min2 max2 min3 max3 min4-equiv max4)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-4-of-nfix-max4

(defthm check-tree-nonleaf-num-range-4-of-nfix-max4
  (equal (check-tree-nonleaf-num-range-4
              tree rulename? min1 max1
              min2 max2 min3 max3 min4 (nfix max4))
         (check-tree-nonleaf-num-range-4
              tree rulename? min1
              max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max4

(defthm check-tree-nonleaf-num-range-4-nat-equiv-congruence-on-max4
  (implies (acl2::nat-equiv max4 max4-equiv)
           (equal (check-tree-nonleaf-num-range-4
                       tree rulename?
                       min1 max1 min2 max2 min3 max3 min4 max4)
                  (check-tree-nonleaf-num-range-4
                       tree rulename? min1 max1
                       min2 max2 min3 max3 min4 max4-equiv)))
  :rule-classes :congruence)