		Search-engine friendly clone of the ACL2 documentation.

Logops-recursive-definitions-theory

Logops-recursive-helpers

Some additional lemmas that are included in logops-recursive-definitions-theory to help with inducting over the definitions of logical operations.

Definitions and Theorems

Theorem: falsify-unsigned-byte-p

(defthm falsify-unsigned-byte-p
  (implies (or (not (integerp size))
               (< size 0)
               (not (integerp i)))
           (not (unsigned-byte-p size i))))

Theorem: falsify-signed-byte-p

(defthm falsify-signed-byte-p
  (implies (or (not (integerp size))
               (not (> size 0))
               (not (integerp i)))
           (not (signed-byte-p size i))))