• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
        • Logops
          • Logops-lemmas
            • Logops-recursive-definitions-theory
              • Basic-logops-induction-schemes
              • Logops-recursive-helpers
              • Unsigned-byte-p*
              • Signed-byte-p*
              • Logxor*
              • Logtail*
              • Lognot*
              • Logmaskp*
              • Logior*
              • Loghead*
              • Logext*
              • Logbitp*
              • Logapp*
              • Logand*
              • Integer-length*
              • Ash*
            • Ihs/logbitp-lemmas
            • Ihs/loghead-lemmas
            • Ihs/logtail-lemmas
            • Ihs/logrpl-lemmas
            • Ihs/logand-lemmas
            • Ihs/logapp-lemmas
            • Ihs/logcar-lemmas
            • Ihs/integer-length-lemmas
            • Ihs/unsigned-byte-p-lemmas
            • Ihs/logext-lemmas
            • Ihs/logcons-lemmas
            • Signed-byte-p-logops
            • Ihs/logxor-lemmas
            • Ihs/logior-lemmas
            • Ihs/logextu-lemmas
            • Ihs/signed-byte-p-lemmas
            • Ihs/lognotu-lemmas
            • Ihs/lognot-lemmas
            • Ihs/logmaskp-lemmas
            • Ihs/ash-lemmas
            • Logops-lemmas-theory
            • Ihs/wrb-lemmas
            • Ihs/logite-lemmas
      • Rtl
    • Algebra
  • Testing-utilities

• Lognot
• Logops-recursive-definitions-theory

Lognot*

Recursive definition of lognot.

Definitions and Theorems

Theorem: lognot*

(defthm lognot*
  (implies (force (integerp i))
           (equal (lognot i)
                  (logcons (b-not (logcar i))
                           (lognot (logcdr i)))))
  :rule-classes ((:definition :clique (lognot)
                              :controller-alist ((lognot t)))))