• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
          • Logxor-defaults
          • Logior-defaults
          • Logbitp-defaults
          • Logand-defaults
          • Ash-defaults
          • Lognot-default
          • Logcdr-default
          • Logcar-default
          • Integer-length-default
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Bitops/defaults
• Logbitp

Logbitp-defaults

Behavior of logbitp on bad inputs.

Definitions and Theorems

Theorem: logbitp-default-1

(defthm logbitp-default-1
  (implies (not (natp a))
           (equal (logbitp a x) (logbitp 0 x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: logbitp-default-2

(defthm logbitp-default-2
  (implies (not (integerp x))
           (equal (logbitp a x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))