		Search-engine friendly clone of the ACL2 documentation.

3vec

3vec-p

Recognizer for 3vecs (with a 4vec-p guard).

Signature
(3vec-p x) → bool
Arguments: x — Guard (4vec-p x).

Definitions and Theorems

Function: 3vec-p

(defun 3vec-p (x)
  (declare (xargs :guard (4vec-p x)))
  (let ((__function__ '3vec-p))
    (declare (ignorable __function__))
    (mbe :logic
         (b* (((4vec x) x))
           (eql (logand x.lower (lognot x.upper))
                0))
         :exec
         (if (atom x)
             t
           (b* (((4vec x) x))
             (eql (logandc2 x.lower x.upper) 0))))))

Theorem: 3vec-p-implies-bits

(defthm 3vec-p-implies-bits
  (and (implies (and (3vec-p x)
                     (not (logbitp n (4vec->upper x))))
                (not (logbitp n (4vec->lower x))))
       (implies (and (3vec-p x)
                     (logbitp n (4vec->lower x)))
                (logbitp n (4vec->upper x)))))