Check if an ABNF is a leaf tree with a single natural number in one of three given ranges, returning that natural number if successful.
(check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) → nat
Function:
(defun check-tree-num-range-3 (tree min1 max1 min2 max2 min3 max3) (declare (xargs :guard (and (abnf::treep tree) (natp min1) (natp max1) (natp min2) (natp max2) (natp min3) (natp max3)))) (let ((__function__ 'check-tree-num-range-3)) (declare (ignorable __function__)) (b* ((min1 (nfix min1)) (max1 (nfix max1)) (min2 (nfix min2)) (max2 (nfix max2)) (min3 (nfix min3)) (max3 (nfix max3)) (error (reserrf (list :required (list :ranges (list min1 max1) (list min2 max2) (list min3 max3)) :found (tree-info-for-error tree)))) ((okf nats) (check-tree-leafterm tree)) ((unless (and (consp nats) (endp (cdr nats)))) error) (nat (car nats)) ((unless (or (and (<= min1 nat) (<= nat max1)) (and (<= min2 nat) (<= nat max2)) (and (<= min3 nat) (<= nat max3)))) error)) nat)))
Theorem:
(defthm nat-resultp-of-check-tree-num-range-3 (b* ((nat (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3))) (nat-resultp nat)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-check-tree-num-range-3 (b* ((acl2::?nat (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3))) (implies (not (reserrp nat)) (natp nat))) :rule-classes :forward-chaining)
Theorem:
(defthm check-tree-num-range-3-bounds (b* ((acl2::?nat (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3))) (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)))))) :rule-classes nil)
Theorem:
(defthm check-tree-num-range-3-of-tree-fix-tree (equal (check-tree-num-range-3 (abnf::tree-fix tree) min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree-equiv min1 max1 min2 max2 min3 max3))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-range-3-of-nfix-min1 (equal (check-tree-num-range-3 tree (nfix min1) max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-nat-equiv-congruence-on-min1 (implies (acl2::nat-equiv min1 min1-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1-equiv max1 min2 max2 min3 max3))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-range-3-of-nfix-max1 (equal (check-tree-num-range-3 tree min1 (nfix max1) min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-nat-equiv-congruence-on-max1 (implies (acl2::nat-equiv max1 max1-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1-equiv min2 max2 min3 max3))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-range-3-of-nfix-min2 (equal (check-tree-num-range-3 tree min1 max1 (nfix min2) max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-nat-equiv-congruence-on-min2 (implies (acl2::nat-equiv min2 min2-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2-equiv max2 min3 max3))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-range-3-of-nfix-max2 (equal (check-tree-num-range-3 tree min1 max1 min2 (nfix max2) min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-nat-equiv-congruence-on-max2 (implies (acl2::nat-equiv max2 max2-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2-equiv min3 max3))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-range-3-of-nfix-min3 (equal (check-tree-num-range-3 tree min1 max1 min2 max2 (nfix min3) max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-nat-equiv-congruence-on-min3 (implies (acl2::nat-equiv min3 min3-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3-equiv max3))) :rule-classes :congruence)
Theorem:
(defthm check-tree-num-range-3-of-nfix-max3 (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 (nfix max3)) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3)))
Theorem:
(defthm check-tree-num-range-3-nat-equiv-congruence-on-max3 (implies (acl2::nat-equiv max3 max3-equiv) (equal (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3) (check-tree-num-range-3 tree min1 max1 min2 max2 min3 max3-equiv))) :rule-classes :congruence)