		Search-engine friendly clone of the ACL2 documentation.

Ihs/logtail-lemmas

Lemmas about logtail from the logops-lemmas book.

Definitions and Theorems

Theorem: logtail-identity

(defthm logtail-identity
  (implies (unsigned-byte-p size i)
           (equal (logtail size i) 0)))

Theorem: logtail-logtail

(defthm logtail-logtail
  (implies (and (force (>= pos1 0))
                (force (integerp pos1))
                (logtail-guard pos i))
           (equal (logtail pos1 (logtail pos i))
                  (logtail (+ pos pos1) i))))

Theorem: logtail-0-i

(defthm logtail-0-i
  (implies (integerp i)
           (equal (logtail 0 i) i)))

Theorem: logtail-size-0

(defthm logtail-size-0
  (implies (and (integerp size) (>= size 0))
           (equal (logtail size 0) 0)))

Theorem: logtail-leq

(defthm logtail-leq
  (implies (and (>= i 0) (logtail-guard pos i))
           (<= (logtail pos i) i))
  :rule-classes ((:linear :trigger-terms ((logtail pos i)))))

Theorem: logtail-equal-0

(defthm logtail-equal-0
  (implies (logtail-guard pos i)
           (equal (equal (logtail pos i) 0)
                  (unsigned-byte-p pos i))))

Theorem: logtail-lessp

(defthm logtail-lessp
  (implies (and (logtail-guard pos i)
                (force (integerp j)))
           (equal (< (logtail pos i) j)
                  (< i (* j (expt 2 pos))))))

Theorem: logtail-unsigned-byte-p

(defthm logtail-unsigned-byte-p
  (implies (and (>= size1 0)
                (integerp size1)
                (logtail-guard size i))
           (equal (unsigned-byte-p size1 (logtail size i))
                  (unsigned-byte-p (+ size size1) i))))

Theorem: logtail-loghead

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

Theorem: logtail-logapp

(defthm logtail-logapp
  (implies (and (logapp-guard size1 i j)
                (force (integerp size))
                (force (>= size 0)))
           (equal (logtail size (logapp size1 i j))
                  (if (< size size1)
                      (logapp (- size1 size)
                              (logtail size i)
                              j)
                    (logtail (- size size1) j)))))

Theorem: logtail-logrpl

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