		Search-engine friendly clone of the ACL2 documentation.

Logext*

Recursive definition of logext.

Definitions and Theorems

Theorem: logext*

(defthm logext*
  (implies
       (logext-guard size i)
       (equal (logext size i)
              (cond ((equal size 1)
                     (if (equal (logcar i) 0) 0 -1))
                    (t (logcons (logcar i)
                                (logext (1- size) (logcdr i)))))))
  :rule-classes ((:definition :clique (logext)
                              :controller-alist ((logext t t)))))