• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
      • Sbitsets
        • Sbitset-members
        • Sbitset-pairp
        • Sbitsetp
        • Sbitset-difference
        • Sbitset-intersect
        • Sbitset-union
        • Sbitset-singleton
        • Sbitset-fix
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Sbitsets

Sbitset-fix

(sbitset-fix x) is a basic fixing function for sparse bitsets.

Signature

(sbitset-fix x) → *

Arguments

x — Guard (sbitsetp x).

Definitions and Theorems

Function: sbitset-fix$inline

(defun acl2::sbitset-fix$inline (x)
       (declare (xargs :guard (sbitsetp x)))
       (let ((__function__ 'sbitset-fix))
            (declare (ignorable __function__))
            (mbe :logic (if (sbitsetp x) x nil)
                 :exec x)))

Theorem: true-listp-of-sbitset-fix

(defthm true-listp-of-sbitset-fix
        (true-listp (sbitset-fix x))
        :rule-classes :type-prescription)

Theorem: sbitsetp-of-sbitset-fix

(defthm sbitsetp-of-sbitset-fix
        (sbitsetp (sbitset-fix x)))

Theorem: sbitset-fix-when-sbitsetp

(defthm sbitset-fix-when-sbitsetp
        (implies (sbitsetp x)
                 (equal (sbitset-fix x) x)))