		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-row-repeat-bitcols

Signature
(s32v-row-repeat-bitcols output-bit input-bit input-bits row s32v) → new-s32v
Arguments: output-bit — Guard (natp output-bit).; input-bit — Guard (natp input-bit).; input-bits — Guard (posp input-bits).; row — Guard (natp row).

Definitions and Theorems

Function: s32v-row-repeat-bitcols

(defun s32v-row-repeat-bitcols
       (output-bit input-bit input-bits row s32v)
 (declare (xargs :stobjs (s32v)))
 (declare (xargs :guard (and (natp output-bit)
                             (natp input-bit)
                             (posp input-bits)
                             (natp row))))
 (declare
      (xargs :guard (and (<= input-bits (* 32 (s32v-ncols s32v)))
                         (<= output-bit (* 32 (s32v-ncols s32v)))
                         (< input-bit input-bits)
                         (< row (s32v-nrows s32v)))))
 (let ((__function__ 's32v-row-repeat-bitcols))
   (declare (ignorable __function__))
   (b*
     (((when (mbe :logic (zp (- (* 32 (s32v-ncols s32v))
                                (nfix output-bit)))
                  :exec (eql output-bit (ash (s32v-ncols s32v) 5))))
       s32v)
      (bit (s32v-get-bit row input-bit s32v))
      (s32v (s32v-install-bit row output-bit bit s32v))
      (new-input-bit (+ 1 (lnfix input-bit)))
      (new-input-bit (if (eql new-input-bit (lposfix input-bits))
                         0
                       new-input-bit)))
     (s32v-row-repeat-bitcols (+ 1 (lnfix output-bit))
                              new-input-bit input-bits row s32v))))

Theorem: s32v-nrows-of-s32v-row-repeat-bitcols

(defthm s32v-nrows-of-s32v-row-repeat-bitcols
 (b* ((?new-s32v
           (s32v-row-repeat-bitcols output-bit
                                    input-bit input-bits row s32v)))
   (implies (< (nfix row) (s32v-nrows s32v))
            (equal (len (stobjs::2darr->rows new-s32v))
                   (len (stobjs::2darr->rows s32v))))))

Theorem: s32v-ncols-of-s32v-row-repeat-bitcols

(defthm s32v-ncols-of-s32v-row-repeat-bitcols
 (b* ((?new-s32v
           (s32v-row-repeat-bitcols output-bit
                                    input-bit input-bits row s32v)))
   (equal (stobjs::2darr->ncols new-s32v)
          (stobjs::2darr->ncols s32v))))

Theorem: s32v-row-repeat-bitcols-of-nfix-output-bit

(defthm s32v-row-repeat-bitcols-of-nfix-output-bit
  (equal (s32v-row-repeat-bitcols (nfix output-bit)
                                  input-bit input-bits row s32v)
         (s32v-row-repeat-bitcols output-bit
                                  input-bit input-bits row s32v)))

Theorem: s32v-row-repeat-bitcols-nat-equiv-congruence-on-output-bit

(defthm s32v-row-repeat-bitcols-nat-equiv-congruence-on-output-bit
 (implies
    (nat-equiv output-bit output-bit-equiv)
    (equal (s32v-row-repeat-bitcols output-bit
                                    input-bit input-bits row s32v)
           (s32v-row-repeat-bitcols output-bit-equiv
                                    input-bit input-bits row s32v)))
 :rule-classes :congruence)

Theorem: s32v-row-repeat-bitcols-of-nfix-input-bit

(defthm s32v-row-repeat-bitcols-of-nfix-input-bit
  (equal (s32v-row-repeat-bitcols output-bit (nfix input-bit)
                                  input-bits row s32v)
         (s32v-row-repeat-bitcols output-bit
                                  input-bit input-bits row s32v)))

Theorem: s32v-row-repeat-bitcols-nat-equiv-congruence-on-input-bit

(defthm s32v-row-repeat-bitcols-nat-equiv-congruence-on-input-bit
 (implies
  (nat-equiv input-bit input-bit-equiv)
  (equal
     (s32v-row-repeat-bitcols output-bit
                              input-bit input-bits row s32v)
     (s32v-row-repeat-bitcols output-bit
                              input-bit-equiv input-bits row s32v)))
 :rule-classes :congruence)

Theorem: s32v-row-repeat-bitcols-of-pos-fix-input-bits

(defthm s32v-row-repeat-bitcols-of-pos-fix-input-bits
  (equal (s32v-row-repeat-bitcols output-bit
                                  input-bit (pos-fix input-bits)
                                  row s32v)
         (s32v-row-repeat-bitcols output-bit
                                  input-bit input-bits row s32v)))

Theorem: s32v-row-repeat-bitcols-pos-equiv-congruence-on-input-bits

(defthm s32v-row-repeat-bitcols-pos-equiv-congruence-on-input-bits
 (implies
  (pos-equiv input-bits input-bits-equiv)
  (equal
     (s32v-row-repeat-bitcols output-bit
                              input-bit input-bits row s32v)
     (s32v-row-repeat-bitcols output-bit
                              input-bit input-bits-equiv row s32v)))
 :rule-classes :congruence)

Theorem: s32v-row-repeat-bitcols-of-nfix-row

(defthm s32v-row-repeat-bitcols-of-nfix-row
  (equal (s32v-row-repeat-bitcols output-bit
                                  input-bit input-bits (nfix row)
                                  s32v)
         (s32v-row-repeat-bitcols output-bit
                                  input-bit input-bits row s32v)))

Theorem: s32v-row-repeat-bitcols-nat-equiv-congruence-on-row

(defthm s32v-row-repeat-bitcols-nat-equiv-congruence-on-row
 (implies
  (nat-equiv row row-equiv)
  (equal
     (s32v-row-repeat-bitcols output-bit
                              input-bit input-bits row s32v)
     (s32v-row-repeat-bitcols output-bit
                              input-bit input-bits row-equiv s32v)))
 :rule-classes :congruence)