		Search-engine friendly clone of the ACL2 documentation.

Ihs/logextu-lemmas

Lemmas about logextu from the logops-lemmas book.

Definitions and Theorems

Theorem: logextu-0

(defthm logextu-0
  (implies (logextu-guard 0 ext-size i)
           (equal (logextu 0 ext-size i) 0)))

Theorem: logextu-as-loghead

(defthm logextu-as-loghead
  (implies (and (logextu-guard final-size ext-size i)
                (<= final-size ext-size))
           (equal (loghead final-size (logext ext-size i))
                  (loghead final-size i))))

Theorem: loghead-logextu

(defthm loghead-logextu
  (implies (and (<= ext-size final-size)
                (<= size ext-size)
                (logextu-guard final-size ext-size i)
                (force (integerp size))
                (force (>= size 0)))
           (equal (loghead size (logextu final-size ext-size i))
                  (loghead size i))))