		Search-engine friendly clone of the ACL2 documentation.

Logmaskp*

Recursive definition of logmaskp.

Definitions and Theorems

Theorem: logmaskp*

(defthm logmaskp*
  (equal (logmaskp i)
         (cond ((not (integerp i)) nil)
               ((equal i 0) t)
               ((equal i -1) nil)
               (t (and (equal (logcar i) 1)
                       (logmaskp (logcdr i))))))
  :rule-classes ((:definition :clique (logmaskp)
                              :controller-alist ((logmaskp t)))))