		Search-engine friendly clone of the ACL2 documentation.

Bytep-additional-theorems

Additional theorems about byte.

Theorem: bytep-forward-unsigned-byte-p

(defthm bytep-forward-unsigned-byte-p
  (implies (bytep x)
           (unsigned-byte-p 8 x))
  :rule-classes :forward-chaining)

Theorem: unsigned-byte-p-rewrite-bytep

(defthm unsigned-byte-p-rewrite-bytep
  (equal (unsigned-byte-p 8 x) (bytep x)))

Theorem: natp-when-bytep

(defthm natp-when-bytep
  (implies (bytep x) (natp x))
  :rule-classes :compound-recognizer)