		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-zero-rows

Signature
(s32v-zero-rows row s32v) → new-s32v
Arguments: row — Guard (natp row).

Definitions and Theorems

Function: s32v-zero-rows

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

Theorem: s32v-nrows-of-s32v-zero-rows

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

Theorem: s32v-ncols-of-s32v-zero-rows

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

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

(defthm s32v-zero-rows-of-nfix-row
  (equal (s32v-zero-rows (nfix row) s32v)
         (s32v-zero-rows row s32v)))

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

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