		Search-engine friendly clone of the ACL2 documentation.

Nibblep-additional-theorems

Additional theorems about nibble.

Theorem: nibblep-forward-unsigned-byte-p

(defthm nibblep-forward-unsigned-byte-p
  (implies (nibblep x)
           (unsigned-byte-p 4 x))
  :rule-classes :forward-chaining)

Theorem: unsigned-byte-p-rewrite-nibblep

(defthm unsigned-byte-p-rewrite-nibblep
  (equal (unsigned-byte-p 4 x)
         (nibblep x)))

Theorem: natp-when-nibblep

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