		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

4vmask-to-a4vec-rec

Signature
(4vmask-to-a4vec-rec mask boolmask nextvar) → (mv upper lower)
Arguments: mask — Guard (4vmask-p mask).; boolmask — Guard (integerp boolmask).; nextvar — Guard (natp nextvar).
Returns: upper — Type (nat-bool-listp upper).; lower — Type (nat-bool-listp lower).

Definitions and Theorems

Function: 4vmask-to-a4vec-rec

(defun 4vmask-to-a4vec-rec (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-rec))
    (declare (ignorable __function__))
    (b* ((mask (sparseint-nfix (4vmask-fix mask)))
         (nextvar (lnfix nextvar))
         ((when (sparseint-equal mask 0))
          (mv (aig-sterm t) (aig-sterm nil)))
         ((mv ubit0 ubit1 nextvar)
          (if (eql 1 (sparseint-bit 0 mask))
              (if (logbitp 0 boolmask)
                  (mv nextvar nextvar (+ 1 nextvar))
                (mv nextvar (1+ nextvar) (+ 2 nextvar)))
            (mv t nil nextvar)))
         ((mv rest-upper rest-lower)
          (4vmask-to-a4vec-rec (sparseint-rightshift 1 mask)
                               (logcdr boolmask)
                               nextvar)))
      (mv (aig-scons ubit0 rest-upper)
          (aig-scons ubit1 rest-lower)))))

Theorem: nat-bool-listp-of-4vmask-to-a4vec-rec.upper

(defthm nat-bool-listp-of-4vmask-to-a4vec-rec.upper
  (b* (((mv ?upper ?lower)
        (4vmask-to-a4vec-rec mask boolmask nextvar)))
    (nat-bool-listp upper))
  :rule-classes :rewrite)

Theorem: nat-bool-listp-of-4vmask-to-a4vec-rec.lower

(defthm nat-bool-listp-of-4vmask-to-a4vec-rec.lower
  (b* (((mv ?upper ?lower)
        (4vmask-to-a4vec-rec mask boolmask nextvar)))
    (nat-bool-listp lower))
  :rule-classes :rewrite)

Theorem: true-listp-of-4vmask-to-a4vec-rec-upper

(defthm true-listp-of-4vmask-to-a4vec-rec-upper
  (b* (((mv ?upper ?lower)
        (4vmask-to-a4vec-rec mask boolmask nextvar)))
    (true-listp upper))
  :rule-classes :type-prescription)

Theorem: true-listp-of-4vmask-to-a4vec-rec-lower

(defthm true-listp-of-4vmask-to-a4vec-rec-lower
  (b* (((mv ?upper ?lower)
        (4vmask-to-a4vec-rec mask boolmask nextvar)))
    (true-listp lower))
  :rule-classes :type-prescription)

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

(defthm 4vmask-to-a4vec-rec-lower-bounds
 (and (nat-bool-list-lower-boundp
           nextvar
           (mv-nth 0
                   (4vmask-to-a4vec-rec mask boolmask nextvar)))
      (nat-bool-list-lower-boundp
           nextvar
           (mv-nth 1
                   (4vmask-to-a4vec-rec mask boolmask nextvar))))
 :rule-classes
 ((:forward-chaining
     :trigger-terms ((4vmask-to-a4vec-rec mask boolmask nextvar)))))

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

(defthm 4vmask-to-a4vec-rec-upper-bounds
 (and (nat-bool-list-upper-boundp
           (+ (nfix nextvar)
              (4vmask-to-a4vec-varcount mask boolmask))
           (mv-nth 0
                   (4vmask-to-a4vec-rec mask boolmask nextvar)))
      (nat-bool-list-upper-boundp
           (+ (nfix nextvar)
              (4vmask-to-a4vec-varcount mask boolmask))
           (mv-nth 1
                   (4vmask-to-a4vec-rec mask boolmask nextvar))))
 :rule-classes
 ((:forward-chaining
     :trigger-terms ((4vmask-to-a4vec-rec mask boolmask nextvar)))))

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

(defthm member-4vmask-to-a4vec-rec-vars
 (iff
  (member
   v
   (append
        (nat-bool-list-nats
             (mv-nth 0
                     (4vmask-to-a4vec-rec mask boolmask nextvar)))
        (nat-bool-list-nats
             (mv-nth 1
                     (4vmask-to-a4vec-rec mask boolmask nextvar)))))
  (and (natp v)
       (<= (nfix nextvar) v)
       (< v
          (+ (nfix nextvar)
             (4vmask-to-a4vec-varcount mask boolmask)))))
 :rule-classes nil)

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

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

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

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

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

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

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

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

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

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

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

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