		Search-engine friendly clone of the ACL2 documentation.

A4vec-rev-blocks

Aig-rev-blocks-nss

Signature
(aig-rev-blocks-nss nbits blocksz-lowbits blocksz-bitidx blocksz x) → *
Arguments: nbits — Guard (natp nbits).; blocksz-lowbits — Guard (natp blocksz-lowbits).; blocksz-bitidx — Guard (natp blocksz-bitidx).; blocksz — Guard (true-listp blocksz).; x — Guard (true-listp x).

Definitions and Theorems

Function: aig-rev-blocks-nss

(defun aig-rev-blocks-nss (nbits blocksz-lowbits
                                 blocksz-bitidx blocksz x)
 (declare (xargs :guard (and (natp nbits)
                             (natp blocksz-lowbits)
                             (natp blocksz-bitidx)
                             (true-listp blocksz)
                             (true-listp x))))
 (declare
    (xargs :guard (unsigned-byte-p blocksz-bitidx blocksz-lowbits)))
 (let ((__function__ 'aig-rev-blocks-nss))
  (declare (ignorable __function__))
  (b*
   (((mv head tail end)
     (gl::first/rest/end blocksz))
    (lowbits
         (mbe :logic (loghead blocksz-bitidx (nfix blocksz-lowbits))
              :exec blocksz-lowbits))
    ((when end)
     (aig-ite-bss head (aig-rev-blocks-nns nbits 1 x)
                  (aig-rev-blocks-nns nbits (pos-fix lowbits)
                                      x))))
   (aig-ite-bss
        head
        (aig-rev-blocks-nss nbits
                            (logior (ash 1 (lnfix blocksz-bitidx))
                                    lowbits)
                            (+ 1 (lnfix blocksz-bitidx))
                            tail x)
        (aig-rev-blocks-nss nbits
                            lowbits (+ 1 (lnfix blocksz-bitidx))
                            tail x)))))

Theorem: aig-rev-blocks-nss-correct

(defthm aig-rev-blocks-nss-correct
 (equal (aig-list->s (aig-rev-blocks-nss nbits blocksz-lowbits
                                         blocksz-bitidx blocksz x)
                     env)
        (rev-blocks
             nbits
             (logior (loghead blocksz-bitidx (nfix blocksz-lowbits))
                     (ash (aig-list->s blocksz env)
                          (nfix blocksz-bitidx)))
             (aig-list->s x env))))

Theorem: aig-rev-blocks-nss-of-nfix-nbits

(defthm aig-rev-blocks-nss-of-nfix-nbits
  (equal (aig-rev-blocks-nss (nfix nbits)
                             blocksz-lowbits
                             blocksz-bitidx blocksz x)
         (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx blocksz x)))

Theorem: aig-rev-blocks-nss-nat-equiv-congruence-on-nbits

(defthm aig-rev-blocks-nss-nat-equiv-congruence-on-nbits
  (implies (nat-equiv nbits nbits-equiv)
           (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                                      blocksz-bitidx blocksz x)
                  (aig-rev-blocks-nss nbits-equiv blocksz-lowbits
                                      blocksz-bitidx blocksz x)))
  :rule-classes :congruence)

Theorem: aig-rev-blocks-nss-of-nfix-blocksz-lowbits

(defthm aig-rev-blocks-nss-of-nfix-blocksz-lowbits
  (equal (aig-rev-blocks-nss nbits (nfix blocksz-lowbits)
                             blocksz-bitidx blocksz x)
         (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx blocksz x)))

Theorem: aig-rev-blocks-nss-nat-equiv-congruence-on-blocksz-lowbits

(defthm aig-rev-blocks-nss-nat-equiv-congruence-on-blocksz-lowbits
  (implies (nat-equiv blocksz-lowbits blocksz-lowbits-equiv)
           (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                                      blocksz-bitidx blocksz x)
                  (aig-rev-blocks-nss nbits blocksz-lowbits-equiv
                                      blocksz-bitidx blocksz x)))
  :rule-classes :congruence)

Theorem: aig-rev-blocks-nss-of-nfix-blocksz-bitidx

(defthm aig-rev-blocks-nss-of-nfix-blocksz-bitidx
  (equal (aig-rev-blocks-nss nbits
                             blocksz-lowbits (nfix blocksz-bitidx)
                             blocksz x)
         (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx blocksz x)))

Theorem: aig-rev-blocks-nss-nat-equiv-congruence-on-blocksz-bitidx

(defthm aig-rev-blocks-nss-nat-equiv-congruence-on-blocksz-bitidx
  (implies
       (nat-equiv blocksz-bitidx blocksz-bitidx-equiv)
       (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                                  blocksz-bitidx blocksz x)
              (aig-rev-blocks-nss nbits blocksz-lowbits
                                  blocksz-bitidx-equiv blocksz x)))
  :rule-classes :congruence)

Theorem: aig-rev-blocks-nss-of-list-fix-blocksz

(defthm aig-rev-blocks-nss-of-list-fix-blocksz
  (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx (list-fix blocksz)
                             x)
         (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx blocksz x)))

Theorem: aig-rev-blocks-nss-list-equiv-congruence-on-blocksz

(defthm aig-rev-blocks-nss-list-equiv-congruence-on-blocksz
  (implies
       (list-equiv blocksz blocksz-equiv)
       (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                                  blocksz-bitidx blocksz x)
              (aig-rev-blocks-nss nbits blocksz-lowbits
                                  blocksz-bitidx blocksz-equiv x)))
  :rule-classes :congruence)

Theorem: aig-rev-blocks-nss-of-list-fix-x

(defthm aig-rev-blocks-nss-of-list-fix-x
  (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx blocksz (list-fix x))
         (aig-rev-blocks-nss nbits blocksz-lowbits
                             blocksz-bitidx blocksz x)))

Theorem: aig-rev-blocks-nss-list-equiv-congruence-on-x

(defthm aig-rev-blocks-nss-list-equiv-congruence-on-x
  (implies
       (list-equiv x x-equiv)
       (equal (aig-rev-blocks-nss nbits blocksz-lowbits
                                  blocksz-bitidx blocksz x)
              (aig-rev-blocks-nss nbits blocksz-lowbits
                                  blocksz-bitidx blocksz x-equiv)))
  :rule-classes :congruence)