• 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
            • Open-logbitp-of-const-meta
            • Equal-by-logbitp
            • Equal-by-logbitp-hint
            • Equal-by-logbitp-hammer
            • 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
    • Bitops/equal-by-logbitp

    Equal-by-logbitp-hammer

    Drastic automation for equal-by-logbitp.

    This is an enhanced version of equal-by-logbitp-hint that also enables a bunch of case-splitting rules that allow logbitp to go through functions like ash, loghead, install-bit, etc.