• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
            • Logops-byte-functions
            • Defword
            • Defbytetype
            • Logext
            • Logrev
            • Loghead
            • Logops-bit-functions
            • Logtail
            • Logapp
            • Logsat
            • Binary--
            • Logcdr
            • Logcar
              • Ihs/logcar-lemmas
                • Logcar-default
              • Logbit
              • Logextu
              • Logcons
              • Lshu
              • Logrpl
              • Ashu
              • Logmaskp
              • Lognotu
              • Logmask
              • Imod
              • Ifloor
              • Bfix
              • Bitmaskp
              • Logite
              • Expt2
              • Zbp
              • *logops-functions*
              • Word/bit-macros
              • Logops-definitions-theory
              • Logops-functions
              • Lbfix
              • Logextu-guard
              • Lshu-guard
              • Logtail-guard
              • Logrpl-guard
              • Logrev-guard
              • Lognotu-guard
              • Logmask-guard
              • Loghead-guard
              • Logext-guard
              • Logbit-guard
              • Logapp-guard
              • Ashu-guard
            • Math-lemmas
            • Ihs-theories
            • Ihs-init
            • Logops
          • Rtl
        • Algebra
      • Testing-utilities
    • Logcar
    • Logops-lemmas

    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)))))