		Search-engine friendly clone of the ACL2 documentation.

Ihs/wrb-lemmas

Definitions and Theorems

Theorem: unsigned-byte-p-wrb

(defthm unsigned-byte-p-wrb
  (implies (and (unsigned-byte-p n j)
                (<= (+ (bsp-size bsp) (bsp-position bsp))
                    n)
                (integerp i)
                (integerp n)
                (bspp bsp))
           (unsigned-byte-p n (wrb i bsp j))))