• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
              • 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

• Ash
• Logops-recursive-definitions-theory

Ash*

Recursive definition of ash.

Definitions and Theorems

Theorem: ash*

(defthm ash*
  (equal (ash i count)
         (cond ((zip count) (ifix i))
               ((< count 0)
                (ash (logcdr i) (1+ count)))
               (t (logcons 0 (ash i (1- count))))))
  :rule-classes ((:definition :clique (ash)
                              :controller-alist ((ash nil t)))))