• 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
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
          • Logcollapse
            • Aig-logcollapse-ns
          • Limshift-loghead-of-logapp
          • Limshift-logext-of-logapp
          • Limshift-loghead-of-ash
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Logcollapse

Aig-logcollapse-ns

Signature

(aig-logcollapse-ns n x) → *

Arguments

n — Guard (natp n).

x — Guard (true-listp x).

Definitions and Theorems

Function: aig-logcollapse-ns

(defun aig-logcollapse-ns (n x)
 (declare (xargs :guard (and (natp n) (true-listp x))))
 (let ((__function__ 'aig-logcollapse-ns))
  (declare (ignorable __function__))
  (b* ((n (lnfix n)))
   (aig-logior-ss
       (aig-loghead-ns n x)
       (aig-logapp-nss
            n nil
            (aig-scons (aig-not (aig-=-ss nil (aig-logtail-ns n x)))
                       (aig-sterm nil)))))))

Theorem: aig-logcollapse-ns-correct

(defthm aig-logcollapse-ns-correct
  (equal (aig-list->s (aig-logcollapse-ns n x)
                      env)
         (bitops::logcollapse n (aig-list->s x env))))

Theorem: aig-logcollapse-ns-of-nfix-n

(defthm aig-logcollapse-ns-of-nfix-n
  (equal (aig-logcollapse-ns (nfix n) x)
         (aig-logcollapse-ns n x)))

Theorem: aig-logcollapse-ns-nat-equiv-congruence-on-n

(defthm aig-logcollapse-ns-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (aig-logcollapse-ns n x)
                  (aig-logcollapse-ns n-equiv x)))
  :rule-classes :congruence)

Theorem: aig-logcollapse-ns-of-list-fix-x

(defthm aig-logcollapse-ns-of-list-fix-x
  (equal (aig-logcollapse-ns n (list-fix x))
         (aig-logcollapse-ns n x)))

Theorem: aig-logcollapse-ns-list-equiv-congruence-on-x

(defthm aig-logcollapse-ns-list-equiv-congruence-on-x
  (implies (list-equiv x x-equiv)
           (equal (aig-logcollapse-ns n x)
                  (aig-logcollapse-ns n x-equiv)))
  :rule-classes :congruence)