		Search-engine friendly clone of the ACL2 documentation.

Self-bounds-for-logtail

Lemmas for the bounds of (logtail n a) versus a.

These are lemmas for:

(< (logtail n a) a)
(= a (logtail n a))
(< a (logtail n a))

Definitions and Theorems

Theorem: (< (logtail n a) a)

(defthm |(< (logtail n a) a)|
 (equal (< (logtail n a) a)
        (if (zip a)
            (< 0 a)
          (and (posp a) (posp n))))
 :rule-classes ((:rewrite)
                (:linear :corollary (implies (and (posp a) (posp n))
                                             (< (logtail n a) a)))))

Theorem: (= a (logtail n a))

(defthm |(= a (logtail n a))|
  (equal (= a (logtail n a))
         (if (zip a)
             (equal a 0)
           (or (zp n) (equal a -1)))))

Theorem: (< a (logtail n a))

(defthm |(< a (logtail n a))|
 (equal (< a (logtail n a))
        (if (zip a)
            (< a 0)
          (and (posp n) (< a -1))))
 :rule-classes ((:rewrite)
                (:linear :corollary (implies (and (posp n) (< a -1))
                                             (< a (logtail n a))))))