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