		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-randomize-rows

Signature
(s32v-randomize-rows row s32v state) → (mv new-s32v new-state)
Arguments: row — Guard (natp row).

Definitions and Theorems

Function: s32v-randomize-rows

(defun s32v-randomize-rows (row s32v state)
  (declare (xargs :stobjs (s32v state)))
  (declare (xargs :guard (natp row)))
  (declare (xargs :guard (<= row (s32v-nrows s32v))))
  (let ((__function__ 's32v-randomize-rows))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (s32v-nrows s32v) (nfix row)))
                     :exec (eql row (s32v-nrows s32v))))
          (mv s32v state))
         ((mv s32v state)
          (s32v-randomize (lnfix row)
                          s32v state)))
      (s32v-randomize-rows (+ 1 (lnfix row))
                           s32v state))))

Theorem: s32v-nrows-of-s32v-randomize-rows

(defthm s32v-nrows-of-s32v-randomize-rows
  (b* (((mv ?new-s32v ?new-state)
        (s32v-randomize-rows row s32v state)))
    (equal (len (stobjs::2darr->rows new-s32v))
           (len (stobjs::2darr->rows s32v)))))

Theorem: s32v-ncols-of-s32v-randomize-rows

(defthm s32v-ncols-of-s32v-randomize-rows
  (b* (((mv ?new-s32v ?new-state)
        (s32v-randomize-rows row s32v state)))
    (equal (stobjs::2darr->ncols new-s32v)
           (stobjs::2darr->ncols s32v))))

Theorem: w-state-of-s32v-randomize-rows

(defthm w-state-of-s32v-randomize-rows
  (b* (((mv ?new-s32v ?new-state)
        (s32v-randomize-rows row s32v state)))
    (equal (w new-state) (w state))))

Theorem: s32v-randomize-rows-of-nfix-row

(defthm s32v-randomize-rows-of-nfix-row
  (equal (s32v-randomize-rows (nfix row)
                              s32v state)
         (s32v-randomize-rows row s32v state)))

Theorem: s32v-randomize-rows-nat-equiv-congruence-on-row

(defthm s32v-randomize-rows-nat-equiv-congruence-on-row
  (implies (nat-equiv row row-equiv)
           (equal (s32v-randomize-rows row s32v state)
                  (s32v-randomize-rows row-equiv s32v state)))
  :rule-classes :congruence)