		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-rev-blocks-sss

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

Definitions and Theorems

Function: aig-rev-blocks-sss

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

Theorem: aig-rev-blocks-sss-correct

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

Theorem: aig-rev-blocks-sss-of-nfix-nbits-lowbits

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

Theorem: aig-rev-blocks-sss-nat-equiv-congruence-on-nbits-lowbits

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

Theorem: aig-rev-blocks-sss-of-nfix-nbits-bitidx

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

Theorem: aig-rev-blocks-sss-nat-equiv-congruence-on-nbits-bitidx

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

Theorem: aig-rev-blocks-sss-of-list-fix-nbits

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

Theorem: aig-rev-blocks-sss-list-equiv-congruence-on-nbits

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

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

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

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

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

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

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

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

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