• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
          • Sparseint-impl
          • Sparseint-p
          • Sparseint-binary-bittest
          • Sparseint-concatenate
          • Sparseint-binary-bitop
          • Sparseint-bitite
          • Sparseint-fix
          • Sparseint$-binary-minus
          • Sparseint-trailing-1-count-from
          • Sparseint-trailing-0-count-from
          • Sparseint-equal
          • Sparseint-test-bitorc2
          • Sparseint-test-bitorc1
          • Sparseint-test-bitnand
          • Sparseint-test-bitandc2
          • Sparseint-test-bitandc1
          • Sparseint-test-bitand
          • Sparseint-rightshift
          • Sparseint-bitcount-from
          • Sparseint-test-bitxor
          • Sparseint-test-bitor
          • Sparseint-test-bitnor
          • Sparseint-test-biteqv
          • Sparseint-compare
          • Sparseint-binary-minus
          • Sparseint-sign-ext
          • Sparseint-plus
          • Sparseint-bitandc2
          • Sparseint-bitandc1
          • Sparseint-bitand
          • Sparseint$-leaf-bitlimit
          • Sparseint-bitxor
          • Sparseint-bitorc2
          • Sparseint-bitorc1
          • Sparseint-bitor
          • Sparseint-bitnor
          • Sparseint-bitnand
          • Sparseint-biteqv
          • Sparseint-ash
          • Sparseint-<
          • Sparseint-bit
          • Sparseint-trailing-1-count
            • Sparseint-trailing-0-count
            • Sparseint-unary-minus
            • Sparseint-length
            • Sparseint-bitnot
            • Sparseint-bitcount
            • Int-to-sparseint
            • Sparseint-val
          • Bitops
          • Bv
          • Ihs
          • Rtl
        • Algebra
      • Testing-utilities
    • Sparseint

    Sparseint-trailing-1-count

    Count the trailing consecutive 1s of a sparseint.

    Signature
    (sparseint-trailing-1-count x) → count
    Arguments
    x — Guard (sparseint-p x).
    Returns
    count — Type (natp count).

    Definitions and Theorems

    Function: sparseint-trailing-1-count

    (defun sparseint-trailing-1-count (x)
     (declare (xargs :guard (sparseint-p x)))
     (let ((__function__ 'sparseint-trailing-1-count))
      (declare (ignorable __function__))
      (b*
       ((count (sparseint$-trailing-0-count-rec 0 1 (sparseint-fix x))))
       (or count 0))))

    Theorem: natp-of-sparseint-trailing-1-count

    (defthm natp-of-sparseint-trailing-1-count
      (b* ((count (sparseint-trailing-1-count x)))
        (natp count))
      :rule-classes :type-prescription)

    Theorem: sparseint-trailing-1-count-correct

    (defthm sparseint-trailing-1-count-correct
      (b* ((common-lisp::?count (sparseint-trailing-1-count x)))
        (equal count
               (trailing-1-count (sparseint-val x)))))

    Theorem: sparseint-trailing-1-count-of-sparseint-fix-x

    (defthm sparseint-trailing-1-count-of-sparseint-fix-x
      (equal (sparseint-trailing-1-count (sparseint-fix x))
             (sparseint-trailing-1-count x)))

    Theorem: sparseint-trailing-1-count-sparseint-equiv-congruence-on-x

    (defthm sparseint-trailing-1-count-sparseint-equiv-congruence-on-x
      (implies (sparseint-equiv x x-equiv)
               (equal (sparseint-trailing-1-count x)
                      (sparseint-trailing-1-count x-equiv)))
      :rule-classes :congruence)