		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4vmask-to-a4vec

Signature
(4vmask-to-a4vec mask boolmask nextvar) → res
Arguments: mask — Guard (4vmask-p mask).; boolmask — Guard (integerp boolmask).; nextvar — Guard (natp nextvar).
Returns: res — Type (nat-bool-a4vec-p! res).

Definitions and Theorems

Function: 4vmask-to-a4vec

(defun 4vmask-to-a4vec (mask boolmask nextvar)
  (declare (xargs :guard (and (4vmask-p mask)
                              (integerp boolmask)
                              (natp nextvar))))
  (declare (xargs :guard (not (sparseint-< mask 0))))
  (let ((__function__ '4vmask-to-a4vec))
    (declare (ignorable __function__))
    (b* (((mv upper lower)
          (4vmask-to-a4vec-rec mask boolmask nextvar)))
      (a4vec upper lower))))

Theorem: nat-bool-a4vec-p!-of-4vmask-to-a4vec

(defthm nat-bool-a4vec-p!-of-4vmask-to-a4vec
  (b* ((res (4vmask-to-a4vec mask boolmask nextvar)))
    (nat-bool-a4vec-p! res))
  :rule-classes :rewrite)

Theorem: member-vars-of-4vmask-to-a4vec

(defthm member-vars-of-4vmask-to-a4vec
 (iff
  (member
      v
      (nat-bool-a4vec-vars (4vmask-to-a4vec mask boolmask nextvar)))
  (and (natp v)
       (<= (nfix nextvar) v)
       (< v
          (+ (nfix nextvar)
             (4vmask-to-a4vec-varcount mask boolmask))))))

Theorem: 4vmask-to-a4vec-lower-bounds

(defthm 4vmask-to-a4vec-lower-bounds
  (nat-bool-a4vec-lower-boundp
       nextvar
       (4vmask-to-a4vec mask boolmask nextvar))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((4vmask-to-a4vec mask boolmask nextvar)))))

Theorem: 4vmask-to-a4vec-upper-bounds

(defthm 4vmask-to-a4vec-upper-bounds
  (nat-bool-a4vec-upper-boundp
       (+ (nfix nextvar)
          (4vmask-to-a4vec-varcount mask boolmask))
       (4vmask-to-a4vec mask boolmask nextvar))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((4vmask-to-a4vec mask boolmask nextvar)))))

Theorem: 4vmask-to-a4vec-of-4vmask-fix-mask

(defthm 4vmask-to-a4vec-of-4vmask-fix-mask
  (equal (4vmask-to-a4vec (4vmask-fix mask)
                          boolmask nextvar)
         (4vmask-to-a4vec mask boolmask nextvar)))

Theorem: 4vmask-to-a4vec-4vmask-equiv-congruence-on-mask

(defthm 4vmask-to-a4vec-4vmask-equiv-congruence-on-mask
  (implies (4vmask-equiv mask mask-equiv)
           (equal (4vmask-to-a4vec mask boolmask nextvar)
                  (4vmask-to-a4vec mask-equiv boolmask nextvar)))
  :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-of-ifix-boolmask

(defthm 4vmask-to-a4vec-of-ifix-boolmask
  (equal (4vmask-to-a4vec mask (ifix boolmask)
                          nextvar)
         (4vmask-to-a4vec mask boolmask nextvar)))

Theorem: 4vmask-to-a4vec-int-equiv-congruence-on-boolmask

(defthm 4vmask-to-a4vec-int-equiv-congruence-on-boolmask
  (implies (int-equiv boolmask boolmask-equiv)
           (equal (4vmask-to-a4vec mask boolmask nextvar)
                  (4vmask-to-a4vec mask boolmask-equiv nextvar)))
  :rule-classes :congruence)

Theorem: 4vmask-to-a4vec-of-nfix-nextvar

(defthm 4vmask-to-a4vec-of-nfix-nextvar
  (equal (4vmask-to-a4vec mask boolmask (nfix nextvar))
         (4vmask-to-a4vec mask boolmask nextvar)))

Theorem: 4vmask-to-a4vec-nat-equiv-congruence-on-nextvar

(defthm 4vmask-to-a4vec-nat-equiv-congruence-on-nextvar
  (implies (nat-equiv nextvar nextvar-equiv)
           (equal (4vmask-to-a4vec mask boolmask nextvar)
                  (4vmask-to-a4vec mask boolmask nextvar-equiv)))
  :rule-classes :congruence)