		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Bspp

(bspp bsp) recognizes objects produced by bsp.

Signature
(bspp bsp) → bool

Definitions and Theorems

Function: bspp

(defun bspp (bsp)
  (declare (xargs :guard t))
  (let ((__function__ 'bspp))
    (declare (ignorable __function__))
    (and (consp bsp)
         (integerp (car bsp))
         (>= (car bsp) 0)
         (integerp (cdr bsp))
         (>= (cdr bsp) 0))))

Theorem: bspp-bsp

(defthm bspp-bsp
  (implies (and (integerp size)
                (>= size 0)
                (integerp pos)
                (>= pos 0))
           (bspp (bsp size pos))))