• 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
• Logtail

Self-bounds-for-logtail

Lemmas for the bounds of (logtail n a) versus a.

These are lemmas for:

• (< (logtail n a) a)
• (= a (logtail n a))
• (< a (logtail n a))

Definitions and Theorems

Theorem: (< (logtail n a) a)

(defthm
 |(< (logtail n a) a)|
 (equal (< (logtail n a) a)
        (if (zip a)
            (< 0 a)
            (and (posp a) (posp n))))
 :rule-classes ((:rewrite)
                (:linear :corollary (implies (and (posp a) (posp n))
                                             (< (logtail n a) a)))))

Theorem: (= a (logtail n a))

(defthm |(= a (logtail n a))|
        (equal (= a (logtail n a))
               (if (zip a)
                   (equal a 0)
                   (or (zp n) (equal a -1)))))

Theorem: (< a (logtail n a))

(defthm
 |(< a (logtail n a))|
 (equal (< a (logtail n a))
        (if (zip a)
            (< a 0)
            (and (posp n) (< a -1))))
 :rule-classes ((:rewrite)
                (:linear :corollary (implies (and (posp n) (< a -1))
                                             (< a (logtail n a))))))