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.
(check-tree-nonleaf-num-range-4 tree rulename? min1 max1 min2 max2 min3 max3 min4 max4) → nat
Function:
(defun check-tree-nonleaf-num-range-4 (tree rulename? min1 max1 min2 max2 min3 max3 min4 max4) (declare (xargs :guard (and (abnf::treep tree) (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:
(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:
(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:
(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:
(defthm check-tree-nonleaf-num-range-4-of-tree-fix-tree (equal (check-tree-nonleaf-num-range-4 (abnf::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:
(defthm check-tree-nonleaf-num-range-4-tree-equiv-congruence-on-tree (implies (abnf::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:
(defthm check-tree-nonleaf-num-range-4-of-maybe-string-fix-rulename? (equal (check-tree-nonleaf-num-range-4 tree (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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)