		Search-engine friendly clone of the ACL2 documentation.

Ihs/logcons-lemmas

Basic lemmas relating logcons to logcar and logcdr, from the logops-lemmas book.

Definitions and Theorems

Theorem: logcar-logcons

(defthm logcar-logcons
  (implies (and (bitp b) (integerp i))
           (equal (logcar (logcons b i)) b)))

Theorem: logcdr-logcons

(defthm logcdr-logcons
  (implies (and (bitp b) (integerp i))
           (equal (logcdr (logcons b i)) i)))

Theorem: equal-logcons

(defthm equal-logcons
  (implies (and (integerp i)
                (integerp logcdr)
                (bitp logcar))
           (equal (equal (logcons logcar logcdr) i)
                  (and (equal (logcar i) logcar)
                       (equal (logcdr i) logcdr)))))

Theorem: logcar-logcdr-elim

(defthm logcar-logcdr-elim
  (implies (integerp i)
           (equal (logcons (logcar i) (logcdr i))
                  i))
  :rule-classes (:rewrite :elim))