		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-decimal-digit-to-nat

Abstract a *decimal-digit to a natural number, interpreting the digits in big endian.

Signature
(abs-*-decimal-digit-to-nat trees) → nat
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: nat — Type (nat-resultp nat).

Definitions and Theorems

Function: abs-*-decimal-digit-to-nat-aux

(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: nat-resultp-of-abs-*-decimal-digit-to-nat-aux

(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: abs-*-decimal-digit-to-nat-aux-of-tree-list-fix-trees

(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: abs-*-decimal-digit-to-nat-aux-tree-list-equiv-congruence-on-trees

(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: abs-*-decimal-digit-to-nat-aux-of-nfix-current

(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: abs-*-decimal-digit-to-nat-aux-nat-equiv-congruence-on-current

(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: abs-*-decimal-digit-to-nat

(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: nat-resultp-of-abs-*-decimal-digit-to-nat

(defthm nat-resultp-of-abs-*-decimal-digit-to-nat
  (b* ((nat (abs-*-decimal-digit-to-nat trees)))
    (nat-resultp nat))
  :rule-classes :rewrite)

Theorem: natp-of-abs-*-decimal-digit-to-nat

(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: abs-*-decimal-digit-to-nat-of-tree-list-fix-trees

(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: abs-*-decimal-digit-to-nat-tree-list-equiv-congruence-on-trees

(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)