		Search-engine friendly clone of the ACL2 documentation.

Ihs/logcar-lemmas

Lemmas about logcar from the logops-lemmas book.

Definitions and Theorems

Theorem: logcar-2*i

(defthm logcar-2*i
  (implies (integerp i)
           (equal (logcar (* 2 i)) 0)))

Theorem: logcar-i+2*j

(defthm logcar-i+2*j
  (implies (and (integerp i) (integerp j))
           (and (equal (logcar (+ i (* 2 j)))
                       (logcar i))
                (equal (logcar (+ (* 2 j) i))
                       (logcar i)))))

Theorem: logcdr-2*i

(defthm logcdr-2*i
  (implies (integerp i)
           (equal (logcdr (* 2 i)) i)))

Theorem: logcdr-i+2*j

(defthm logcdr-i+2*j
  (implies (and (integerp i) (integerp j))
           (and (equal (logcdr (+ i (* 2 j)))
                       (+ (logcdr i) j))
                (equal (logcdr (+ (* 2 j) i))
                       (+ (logcdr i) j)))))

Theorem: logcar-loghead

(defthm logcar-loghead
  (implies (loghead-guard size i)
           (equal (logcar (loghead size i))
                  (if (equal size 0) 0 (logcar i)))))

Theorem: logcar-logapp

(defthm logcar-logapp
  (implies (logapp-guard size i j)
           (equal (logcar (logapp size i j))
                  (if (equal size 0)
                      (logcar j)
                    (logcar i)))))

Theorem: logcar-logrpl

(defthm logcar-logrpl
  (implies (logrpl-guard size i j)
           (equal (logcar (logrpl size i j))
                  (if (equal size 0)
                      (logcar j)
                    (logcar i)))))