		Search-engine friendly clone of the ACL2 documentation.

Ihs/logext-lemmas

Lemmas about logext from the logops-lemmas book.

Definitions and Theorems

Theorem: logext-identity

(defthm logext-identity
  (implies (signed-byte-p size i)
           (equal (logext size i) i)))

Theorem: logext-+-cancel

(defthm logext-+-cancel
  (implies (and (integerp size)
                (> size 0)
                (integerp i)
                (integerp j)
                (integerp k))
           (equal (equal (logext size (+ i j))
                         (logext size (+ i k)))
                  (equal (logext size j)
                         (logext size k)))))

Theorem: logext-+-logext

(defthm logext-+-logext
  (implies (and (integerp size)
                (> size 0)
                (integerp i)
                (integerp j))
           (equal (logext size (+ i (logext size j)))
                  (logext size (+ i j)))))