		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-rev-blocks

Signature
(s4vec-rev-blocks nbits blocksz x) → res
Arguments: nbits — Guard (s4vec-p nbits).; blocksz — Guard (s4vec-p blocksz).; x — Guard (s4vec-p x).
Returns: res — Type (s4vec-p res).

Definitions and Theorems

Function: s4vec-rev-blocks

(defun s4vec-rev-blocks (nbits blocksz x)
 (declare (xargs :guard (and (s4vec-p nbits)
                             (s4vec-p blocksz)
                             (s4vec-p x))))
 (let ((__function__ 's4vec-rev-blocks))
  (declare (ignorable __function__))
  (b* (((unless (and (s4vec-2vec-p nbits)
                     (s4vec-2vec-p blocksz)))
        (s4vec-x))
       (nbits-int (s4vec->upper nbits))
       ((when (sparseint-< nbits-int 0))
        (s4vec-x))
       (blocksz-int (s4vec->upper blocksz))
       ((unless (sparseint-< 0 blocksz-int))
        (s4vec-x))
       (nbits-val (s4vec-sparseint-val nbits-int))
       (blocksz-val (s4vec-sparseint-val blocksz-int)))
   (if-s2vec-p
    (x)
    (s2vec
        (sparseint-rev-blocks nbits-val blocksz-val (s2vec->val x)))
    (b* (((s4vec x)))
     (s4vec
          (sparseint-rev-blocks nbits-val blocksz-val x.upper)
          (sparseint-rev-blocks nbits-val blocksz-val x.lower)))))))

Theorem: s4vec-p-of-s4vec-rev-blocks

(defthm s4vec-p-of-s4vec-rev-blocks
  (b* ((res (s4vec-rev-blocks nbits blocksz x)))
    (s4vec-p res))
  :rule-classes :rewrite)

Theorem: s4vec-rev-blocks-correct

(defthm s4vec-rev-blocks-correct
  (b* ((?res (s4vec-rev-blocks nbits blocksz x)))
    (equal (s4vec->4vec res)
           (4vec-rev-blocks (s4vec->4vec nbits)
                            (s4vec->4vec blocksz)
                            (s4vec->4vec x)))))

Theorem: s4vec-rev-blocks-of-s4vec-fix-nbits

(defthm s4vec-rev-blocks-of-s4vec-fix-nbits
  (equal (s4vec-rev-blocks (s4vec-fix nbits)
                           blocksz x)
         (s4vec-rev-blocks nbits blocksz x)))

Theorem: s4vec-rev-blocks-s4vec-equiv-congruence-on-nbits

(defthm s4vec-rev-blocks-s4vec-equiv-congruence-on-nbits
  (implies (s4vec-equiv nbits nbits-equiv)
           (equal (s4vec-rev-blocks nbits blocksz x)
                  (s4vec-rev-blocks nbits-equiv blocksz x)))
  :rule-classes :congruence)

Theorem: s4vec-rev-blocks-of-s4vec-fix-blocksz

(defthm s4vec-rev-blocks-of-s4vec-fix-blocksz
  (equal (s4vec-rev-blocks nbits (s4vec-fix blocksz)
                           x)
         (s4vec-rev-blocks nbits blocksz x)))

Theorem: s4vec-rev-blocks-s4vec-equiv-congruence-on-blocksz

(defthm s4vec-rev-blocks-s4vec-equiv-congruence-on-blocksz
  (implies (s4vec-equiv blocksz blocksz-equiv)
           (equal (s4vec-rev-blocks nbits blocksz x)
                  (s4vec-rev-blocks nbits blocksz-equiv x)))
  :rule-classes :congruence)

Theorem: s4vec-rev-blocks-of-s4vec-fix-x

(defthm s4vec-rev-blocks-of-s4vec-fix-x
  (equal (s4vec-rev-blocks nbits blocksz (s4vec-fix x))
         (s4vec-rev-blocks nbits blocksz x)))

Theorem: s4vec-rev-blocks-s4vec-equiv-congruence-on-x

(defthm s4vec-rev-blocks-s4vec-equiv-congruence-on-x
  (implies (s4vec-equiv x x-equiv)
           (equal (s4vec-rev-blocks nbits blocksz x)
                  (s4vec-rev-blocks nbits blocksz x-equiv)))
  :rule-classes :congruence)