		Search-engine friendly clone of the ACL2 documentation.

Ihs/logrpl-lemmas

Lemmas about logrpl from the logops-lemmas book.

Definitions and Theorems

Theorem: logrpl-0

(defthm logrpl-0
  (and (implies (logrpl-guard 0 i j)
                (equal (logrpl 0 i j) j))
       (implies (logrpl-guard size i 0)
                (equal (logrpl size i 0)
                       (loghead size i)))
       (implies (and (unsigned-byte-p size j)
                     (integerp i))
                (equal (logrpl size i j)
                       (loghead size i)))))

Theorem: unsigned-byte-p-logrpl

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

Theorem: logrpl-i-i

(defthm logrpl-i-i
  (implies (logrpl-guard size i i)
           (equal (logrpl size i i) i)))

Theorem: logrpl-loghead-i-i

(defthm logrpl-loghead-i-i
  (implies (and (<= size size1)
                (loghead-guard size1 i)
                (force (integerp size))
                (force (>= size 0)))
           (equal (logrpl size (loghead size1 i) i)
                  i)))

Theorem: logrpl-logrpl-right

(defthm logrpl-logrpl-right
  (implies (and (logrpl-guard size1 j k)
                (logrpl-guard size i (logrpl size1 j k))
                (<= size1 size))
           (equal (logrpl size i (logrpl size1 j k))
                  (logrpl size i k))))

Theorem: logrpl-logrpl-left

(defthm logrpl-logrpl-left
  (implies (and (logrpl-guard size1 i j)
                (logrpl-guard size (logrpl size1 i j) k)
                (<= size size1))
           (equal (logrpl size (logrpl size1 i j) k)
                  (logrpl size i k))))