		Search-engine friendly clone of the ACL2 documentation.

Sbitset-singleton

Sbitset-singleton-pair

(sbitset-singleton-pair a) creates a sbitset-pairp whose only member is a.

Signature
(sbitset-singleton-pair a) → pair
Arguments: a — Guard (natp a).
Returns: pair — Type (sbitset-pairp pair).

Definitions and Theorems

Function: sbitset-singleton-pair$inline

(defun sbitset-singleton-pair$inline (a)
  (declare (type unsigned-byte a))
  (declare (xargs :guard (natp a)))
  (declare (xargs :split-types t))
  (let ((__function__ 'sbitset-singleton-pair))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((a (nfix a)))
           (sbitset-pair (floor a *sbitset-block-size*)
                         (expt 2 (mod a *sbitset-block-size*))))
         :exec (sbitset-pair (truncate a 60)
                             (ash 1 (rem a 60))))))

Theorem: sbitset-pairp-of-sbitset-singleton-pair

(defthm sbitset-pairp-of-sbitset-singleton-pair
  (b* ((pair (sbitset-singleton-pair$inline a)))
    (sbitset-pairp pair))
  :rule-classes :rewrite)

Theorem: sbitset-pair-offset-of-sbitset-singleton-pair

(defthm sbitset-pair-offset-of-sbitset-singleton-pair
  (equal (sbitset-pair-offset (sbitset-singleton-pair a))
         (floor (nfix a) *sbitset-block-size*)))

Theorem: sbiset-pair-block-of-sbitset-singleton-pair

(defthm sbiset-pair-block-of-sbitset-singleton-pair
  (equal (sbitset-pair-block (sbitset-singleton-pair a))
         (expt 2 (mod (nfix a) *sbitset-block-size*))))