Recursive definition of ash.
Theorem: ash*
(defthm ash* (equal (ash i count) (cond ((zip count) (ifix i)) ((< count 0) (ash (logcdr i) (1+ count))) (t (logcons 0 (ash i (1- count)))))) :rule-classes ((:definition :clique (ash) :controller-alist ((ash nil t)))))
