Abstract a
(abs-*-decimal-digit-to-nat trees) → nat
Function:
(defun abs-*-decimal-digit-to-nat-aux (trees current) (declare (xargs :guard (and (abnf::tree-listp trees) (natp current)))) (let ((__function__ 'abs-*-decimal-digit-to-nat-aux)) (declare (ignorable __function__)) (b* (((when (endp trees)) (nfix current)) ((okf digit-nat) (abs-decimal-digit-to-nat (car trees)))) (abs-*-decimal-digit-to-nat-aux (cdr trees) (+ digit-nat (* (nfix current) 10))))))
Theorem:
(defthm nat-resultp-of-abs-*-decimal-digit-to-nat-aux (b* ((nat (abs-*-decimal-digit-to-nat-aux trees current))) (nat-resultp nat)) :rule-classes :rewrite)
Theorem:
(defthm abs-*-decimal-digit-to-nat-aux-of-tree-list-fix-trees (equal (abs-*-decimal-digit-to-nat-aux (abnf::tree-list-fix trees) current) (abs-*-decimal-digit-to-nat-aux trees current)))
Theorem:
(defthm abs-*-decimal-digit-to-nat-aux-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv trees trees-equiv) (equal (abs-*-decimal-digit-to-nat-aux trees current) (abs-*-decimal-digit-to-nat-aux trees-equiv current))) :rule-classes :congruence)
Theorem:
(defthm abs-*-decimal-digit-to-nat-aux-of-nfix-current (equal (abs-*-decimal-digit-to-nat-aux trees (nfix current)) (abs-*-decimal-digit-to-nat-aux trees current)))
Theorem:
(defthm abs-*-decimal-digit-to-nat-aux-nat-equiv-congruence-on-current (implies (acl2::nat-equiv current current-equiv) (equal (abs-*-decimal-digit-to-nat-aux trees current) (abs-*-decimal-digit-to-nat-aux trees current-equiv))) :rule-classes :congruence)
Function:
(defun abs-*-decimal-digit-to-nat (trees) (declare (xargs :guard (abnf::tree-listp trees))) (let ((__function__ 'abs-*-decimal-digit-to-nat)) (declare (ignorable __function__)) (abs-*-decimal-digit-to-nat-aux trees 0)))
Theorem:
(defthm nat-resultp-of-abs-*-decimal-digit-to-nat (b* ((nat (abs-*-decimal-digit-to-nat trees))) (nat-resultp nat)) :rule-classes :rewrite)
Theorem:
(defthm natp-of-abs-*-decimal-digit-to-nat (b* ((acl2::?nat (abs-*-decimal-digit-to-nat trees))) (implies (not (reserrp nat)) (natp nat))) :rule-classes :forward-chaining)
Theorem:
(defthm abs-*-decimal-digit-to-nat-of-tree-list-fix-trees (equal (abs-*-decimal-digit-to-nat (abnf::tree-list-fix trees)) (abs-*-decimal-digit-to-nat trees)))
Theorem:
(defthm abs-*-decimal-digit-to-nat-tree-list-equiv-congruence-on-trees (implies (abnf::tree-list-equiv trees trees-equiv) (equal (abs-*-decimal-digit-to-nat trees) (abs-*-decimal-digit-to-nat trees-equiv))) :rule-classes :congruence)