		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4vmask-to-a4vec-env

Signature
(4vmask-to-a4vec-env mask boolmask val nextvar) → env
Arguments: mask — Guard (4vmask-p mask).; boolmask — Guard (integerp boolmask).; val — Guard (4vec-p val).; nextvar — Guard (natp nextvar).

Definitions and Theorems

Function: 4vmask-to-a4vec-env

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

Theorem: key-exists-in-4vmask-to-a4vec-env

(defthm key-exists-in-4vmask-to-a4vec-env
 (iff
  (hons-assoc-equal v
                    (4vmask-to-a4vec-env mask boolmask val nextvar))
  (and (natp v)
       (<= (nfix nextvar) v)
       (< v
          (+ (nfix nextvar)
             (4vmask-to-a4vec-varcount mask boolmask))))))

Theorem: eval-4vmask-to-a4vec-with-env

(defthm eval-4vmask-to-a4vec-with-env
  (b* ((vala (4vmask-to-a4vec mask boolmask nextvar))
       (env (4vmask-to-a4vec-env mask boolmask val nextvar)))
    (implies (and (4vec-boolmaskp val boolmask)
                  (4vmask-p mask)
                  (natp (sparseint-val mask)))
             (equal (4vec-mask mask (a4vec-eval vala env))
                    (4vec-mask mask val)))))

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

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

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

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

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

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

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

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

Theorem: 4vmask-to-a4vec-env-of-4vec-fix-val

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

Theorem: 4vmask-to-a4vec-env-4vec-equiv-congruence-on-val

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

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

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

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

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