|
|
|---|
|
|
|
|---|
Recursive definition of logbitp.
Theorem:
(defthm logbitp* (implies (and (integerp pos) (>= pos 0) (integerp i)) (equal (logbitp pos i) (cond ((equal pos 0) (equal (logcar i) 1)) (t (logbitp (1- pos) (logcdr i)))))) :rule-classes ((:definition :clique (logbitp) :controller-alist ((logbitp t t)))))