		Search-engine friendly clone of the ACL2 documentation.

Ihs/logmaskp-lemmas

Lemmas about logmaskp from the logops-lemmas book.

Definitions and Theorems

Theorem: logmaskp-expt-2-n-minus-1

(defthm logmaskp-expt-2-n-minus-1
  (implies (and (force (integerp n)) (>= n 0))
           (logmaskp (+ -1 (expt 2 n)))))

Theorem: logmaskp-logmask

(defthm logmaskp-logmask
  (implies (logmask-guard n)
           (logmaskp (logmask n))))

Theorem: logand-with-mask

(defthm logand-with-mask
  (implies (and (logmaskp mask)
                (equal size (integer-length mask))
                (force (integerp i)))
           (equal (logand mask i)
                  (loghead size i))))