		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-*bit

A list of zero or more BIT parse trees is abstracted to the big-endian value of its bits.

Signature
(abstract-*bit trees) → nat
Arguments: trees — Guard (tree-listp trees).
Returns: nat — Type (natp nat).

Definitions and Theorems

Function: abstract-*bit-aux

(defun abstract-*bit-aux (trees accumulator)
  (declare (xargs :guard (and (tree-listp trees)
                              (natp accumulator))))
  (b* (((when (endp trees)) (nfix accumulator))
       (bit (abstract-bit (car trees))))
    (abstract-*bit-aux (cdr trees)
                       (+ (* 2 accumulator) bit))))

Theorem: natp-of-abstract-*bit-aux

(defthm natp-of-abstract-*bit-aux
  (b* ((nat (abstract-*bit-aux trees accumulator)))
    (natp nat))
  :rule-classes :rewrite)

Function: abstract-*bit

(defun abstract-*bit (trees)
  (declare (xargs :guard (tree-listp trees)))
  (abstract-*bit-aux trees 0))

Theorem: natp-of-abstract-*bit

(defthm natp-of-abstract-*bit
  (b* ((nat (abstract-*bit trees)))
    (natp nat))
  :rule-classes :rewrite)