		Search-engine friendly clone of the ACL2 documentation.

Ihs/logapp-lemmas

Lemmas about logapp from the logops-lemmas book.

Definitions and Theorems

Theorem: logapp-0

(defthm logapp-0
  (and (implies (logapp-guard size i 0)
                (equal (logapp size i 0)
                       (loghead size i)))
       (implies (logapp-guard size 0 i)
                (equal (logapp size 0 i)
                       (* i (expt 2 size))))
       (implies (logapp-guard 0 i j)
                (equal (logapp 0 i j) j))))

Theorem: unsigned-byte-p-logapp

(defthm unsigned-byte-p-logapp
  (implies (and (<= size1 size)
                (>= j 0)
                (logapp-guard size1 i j)
                (force (integerp size))
                (force (>= size 0)))
           (equal (unsigned-byte-p size (logapp size1 i j))
                  (unsigned-byte-p (- size size1) j))))

Theorem: associativity-of-logapp

(defthm associativity-of-logapp
  (implies (and (logapp-guard size1 j k)
                (logapp-guard size i (logapp size1 j k)))
           (equal (logapp size i (logapp size1 j k))
                  (logapp (+ size size1)
                          (logapp size i j)
                          k))))

Theorem: logapp-loghead-logtail

(defthm logapp-loghead-logtail
  (implies (logapp-guard size i i)
           (equal (logapp size (loghead size i)
                          (logtail size i))
                  i)))

Theorem: loghead-logapp-loghead-logtail

(defthm loghead-logapp-loghead-logtail
  (implies (and (loghead-guard size i)
                (loghead-guard size1 i))
           (equal (logapp size (loghead size i)
                          (loghead size1 (logtail size i)))
                  (loghead (+ size size1) i))))