• 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

Logops-lemmas

A book of lemmas about logical operations on numbers.

Subtopics

Logops-recursive-definitions-theory
Recursive equivalents of logical operations.
Ihs/logbitp-lemmas
Lemmas about logbitp and logbit from the logops-lemmas book.
Ihs/logtail-lemmas
Lemmas about logtail from the logops-lemmas book.
Ihs/loghead-lemmas
Lemmas about loghead from the logops-lemmas book.
Ihs/logrpl-lemmas
Lemmas about logrpl from the logops-lemmas book.
Ihs/logand-lemmas
Lemmas about logand from the logops-lemmas book.
Ihs/logapp-lemmas
Lemmas about logapp from the logops-lemmas book.
Ihs/logcar-lemmas
Lemmas about logcar from the logops-lemmas book.
Ihs/integer-length-lemmas
Lemmas about integer-length from the logops-lemmas book.
Ihs/unsigned-byte-p-lemmas
Lemmas about unsigned-byte-p from the logops-lemmas book.
Ihs/logcons-lemmas
Basic lemmas relating logcons to logcar and logcdr, from the logops-lemmas book.
Signed-byte-p-logops
Lemmas showing the basic preservation of signed-byte-p by operations like logand, logior, etc.
Ihs/logxor-lemmas
Lemmas about logxor from the logops-lemmas book.
Ihs/logior-lemmas
Lemmas about logior from the logops-lemmas book.
Ihs/logext-lemmas
Lemmas about logext from the logops-lemmas book.
Ihs/logextu-lemmas
Lemmas about logextu from the logops-lemmas book.
Ihs/signed-byte-p-lemmas
Lemmas about signed-byte-p from the logops-lemmas book.
Ihs/lognotu-lemmas
Lemmas about lognotu from the logops-lemmas book.
Ihs/lognot-lemmas
Lemmas about lognot from the logops-lemmas book.
Ihs/logmaskp-lemmas
Lemmas about logmaskp from the logops-lemmas book.
Ihs/ash-lemmas
Lemmas about ash from the logops-lemmas book.
Logops-lemmas-theory
The "minimal" theory for the logops-lemmas book.
Ihs/wrb-lemmas
Ihs/logite-lemmas
Lemmas about logite from the logops-lemmas book.