• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
      • 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
          • Logbitp-mismatch
          • Trailing-1-count
          • Bitops/rotate
          • Bitops/equal-by-logbitp
          • Bitops/ash-bounds
            • Self-bounds-for-ash
            • Self-bounds-for-logtail
            • Monotonicity-properties-of-ash
            • (= 0 (ash 1 x))
            • 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
    • Bitops/ash-bounds
    • Ash

    (= 0 (ash 1 x))

    Definitions and Theorems

    Theorem: (= 0 (ash 1 x))

    (defthm |(= 0 (ash 1 x))|
        (equal (equal 0 (ash 1 x)) (negp x)))