		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

V2i-first-n

Signature
(v2i-first-n n v) → v2i
Arguments: n — Guard (natp n).; v — Guard (true-listp v).
Returns: v2i — Type (equal v2i (gl::v2i (take n v))).

Definitions and Theorems

Function: v2i-first-n

(defun v2i-first-n (n v)
  (declare (xargs :guard (and (natp n) (true-listp v))))
  (let ((__function__ 'v2i-first-n))
    (declare (ignorable __function__))
    (cond ((zp n) (gl::bool->sign nil))
          ((eql n 1) (gl::bool->sign (car v)))
          (t (logapp 1 (bool->bit (car v))
                     (v2i-first-n (1- n) (cdr v)))))))

Theorem: return-type-of-v2i-first-n

(defthm return-type-of-v2i-first-n
  (b* ((v2i (v2i-first-n n v)))
    (equal v2i (gl::v2i (take n v))))
  :rule-classes :rewrite)

Theorem: v2i-first-n-of-nfix-n

(defthm v2i-first-n-of-nfix-n
  (equal (v2i-first-n (nfix n) v)
         (v2i-first-n n v)))

Theorem: v2i-first-n-nat-equiv-congruence-on-n

(defthm v2i-first-n-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (v2i-first-n n v)
                  (v2i-first-n n-equiv v)))
  :rule-classes :congruence)

Theorem: v2i-first-n-of-list-fix-v

(defthm v2i-first-n-of-list-fix-v
  (equal (v2i-first-n n (list-fix v))
         (v2i-first-n n v)))

Theorem: v2i-first-n-list-equiv-congruence-on-v

(defthm v2i-first-n-list-equiv-congruence-on-v
  (implies (list-equiv v v-equiv)
           (equal (v2i-first-n n v)
                  (v2i-first-n n v-equiv)))
  :rule-classes :congruence)