Abstract a
(abs-decimal-digit-to-nat tree) → nat
Function:
(defun abs-decimal-digit-to-nat (tree) (declare (xargs :guard (abnf::treep tree))) (let ((__function__ 'abs-decimal-digit-to-nat)) (declare (ignorable __function__)) (b* (((okf nat) (check-tree-nonleaf-num-range tree "digit" 48 57))) (- nat 48))))
Theorem:
(defthm nat-resultp-of-abs-decimal-digit-to-nat (b* ((nat (abs-decimal-digit-to-nat tree))) (nat-resultp nat)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-decimal-digit-to-nat (b* ((acl2::?nat (abs-decimal-digit-to-nat tree))) (implies (not (reserrp nat)) (natp nat))) :rule-classes :forward-chaining)
Theorem:
(defthm abs-decimal-digit-to-nat-bound (b* ((acl2::?nat (abs-decimal-digit-to-nat tree))) (implies (not (reserrp nat)) (< nat 10))) :rule-classes :linear)
Theorem:
(defthm abs-decimal-digit-to-nat-of-tree-fix-tree (equal (abs-decimal-digit-to-nat (abnf::tree-fix tree)) (abs-decimal-digit-to-nat tree)))
Theorem:
(defthm abs-decimal-digit-to-nat-tree-equiv-congruence-on-tree (implies (abnf::tree-equiv tree tree-equiv) (equal (abs-decimal-digit-to-nat tree) (abs-decimal-digit-to-nat tree-equiv))) :rule-classes :congruence)