• 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
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
        • Logops
          • Logops-lemmas
            • Logops-recursive-definitions-theory
            • Ihs/logbitp-lemmas
            • Ihs/logtail-lemmas
            • Ihs/loghead-lemmas
            • Ihs/logrpl-lemmas
            • Ihs/logand-lemmas
            • Ihs/logapp-lemmas
            • Ihs/logcar-lemmas
            • Ihs/integer-length-lemmas
            • Ihs/unsigned-byte-p-lemmas
            • Ihs/logcons-lemmas
            • Signed-byte-p-logops
            • Ihs/logxor-lemmas
            • Ihs/logior-lemmas
            • Ihs/logext-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

• Logops-lemmas

Logops-lemmas-theory

The "minimal" theory for the logops-lemmas book.

This theory contains the theory logops-definitions-theory, plus all of the lemmas meant to be exported by the logops-lemmas book.