		Search-engine friendly clone of the ACL2 documentation.

A4vec-rev-blocks

Aig-rev-blocks-nns

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

Definitions and Theorems

Function: aig-rev-blocks-nns

(defun aig-rev-blocks-nns (nbits blocksz x)
 (declare (xargs :guard (and (natp nbits)
                             (posp blocksz)
                             (true-listp x))))
 (let ((__function__ 'aig-rev-blocks-nns))
   (declare (ignorable __function__))
   (b*
    ((nbits (lnfix nbits))
     (blocksz (lposfix blocksz))
     ((when (< nbits blocksz))
      (aig-loghead-ns nbits x))
     (next-nbits (- nbits blocksz))
     (rest (aig-rev-blocks-nns next-nbits
                               blocksz (aig-logtail-ns blocksz x))))
    (aig-logapp-nss next-nbits
                    rest (aig-loghead-ns blocksz x)))))

Theorem: aig-rev-blocks-nns-correct

(defthm aig-rev-blocks-nns-correct
  (equal (aig-list->s (aig-rev-blocks-nns nbits blocksz x)
                      env)
         (rev-blocks nbits blocksz (aig-list->s x env))))

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

(defthm aig-rev-blocks-nns-of-nfix-nbits
  (equal (aig-rev-blocks-nns (nfix nbits)
                             blocksz x)
         (aig-rev-blocks-nns nbits blocksz x)))

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

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

Theorem: aig-rev-blocks-nns-of-pos-fix-blocksz

(defthm aig-rev-blocks-nns-of-pos-fix-blocksz
  (equal (aig-rev-blocks-nns nbits (pos-fix blocksz)
                             x)
         (aig-rev-blocks-nns nbits blocksz x)))

Theorem: aig-rev-blocks-nns-pos-equiv-congruence-on-blocksz

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

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

(defthm aig-rev-blocks-nns-of-list-fix-x
  (equal (aig-rev-blocks-nns nbits blocksz (list-fix x))
         (aig-rev-blocks-nns nbits blocksz x)))

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

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