|
|
|---|
|
|
|
|---|
Recursive definition of integer-length.
Theorem:
(defthm integer-length* (equal (integer-length i) (cond ((zip i) 0) ((equal i -1) 0) (t (1+ (integer-length (logcdr i)))))) :rule-classes ((:definition :clique (integer-length) :controller-alist ((integer-length t)))))