Lemmas about unsigned-byte-p from the logops-lemmas book.
Theorem:
(defthm unsigned-byte-p-base-case (equal (unsigned-byte-p size 0) (and (integerp size) (<= 0 size))))
Theorem:
(defthm unsigned-byte-p-0 (equal (unsigned-byte-p 0 x) (equal x 0)))
Theorem:
(defthm unsigned-byte-p-plus (implies (and (unsigned-byte-p size i) (>= j 0) (integerp j)) (and (unsigned-byte-p (+ size j) i) (unsigned-byte-p (+ j size) i))))
Theorem:
(defthm difference-unsigned-byte-p (implies (and (unsigned-byte-p size i) (<= j i) (>= j 0) (integerp j)) (and (unsigned-byte-p size (- i j)) (unsigned-byte-p size (+ (- j) i)))))
Theorem:
(defthm floor-unsigned-byte-p (implies (and (> x 1) (force (real/rationalp x)) (unsigned-byte-p size i)) (unsigned-byte-p size (floor i x))))