Equivalences between digits and bytes.
These rules are disabled by default. They can be selectively enabled for specific proofs as needed.
Note that the converse equalities
would include
Theorem:
(defthm unsigned-byte-p-rewrite-dab-digitp (implies (posp n) (equal (unsigned-byte-p n x) (dab-digitp (expt 2 n) x))))
Theorem:
(defthm unsigned-byte-listp-rewrite-dab-digit-listp (implies (posp n) (equal (unsigned-byte-listp n x) (dab-digit-listp (expt 2 n) x))))