		Search-engine friendly clone of the ACL2 documentation.

Fraig

S32v-bitcol-nth-set

Signature
(s32v-bitcol-nth-set row nleft bitcol s32v) → nth-row
Arguments: row — Guard (natp row).; nleft — Guard (natp nleft).; bitcol — Guard (natp bitcol).
Returns: nth-row — Type (natp nth-row).

Definitions and Theorems

Function: s32v-bitcol-nth-set

(defun s32v-bitcol-nth-set (row nleft bitcol s32v)
 (declare (xargs :stobjs (s32v)))
 (declare (xargs :guard (and (natp row)
                             (natp nleft)
                             (natp bitcol))))
 (declare
   (xargs
        :guard (and (<= row (s32v-nrows s32v))
                    (< bitcol (* 32 (s32v-ncols s32v)))
                    (< nleft
                       (s32v-bitcol-count-set row 0 bitcol s32v)))))
 (let ((__function__ 's32v-bitcol-nth-set))
   (declare (ignorable __function__))
   (b* ((bit (s32v-get-bit row bitcol s32v))
        ((when (and (eql (lnfix nleft) 0) (eql bit 1)))
         (lnfix row))
        ((unless (mbt (posp (s32v-bitcol-count-set (+ 1 (lnfix row))
                                                   0 bitcol s32v))))
         (lnfix row)))
     (s32v-bitcol-nth-set (1+ (lnfix row))
                          (- (lnfix nleft) bit)
                          bitcol s32v))))

Theorem: natp-of-s32v-bitcol-nth-set

(defthm natp-of-s32v-bitcol-nth-set
  (b* ((nth-row (s32v-bitcol-nth-set row nleft bitcol s32v)))
    (natp nth-row))
  :rule-classes :type-prescription)

Theorem: s32v-bitcol-nth-set-bound

(defthm s32v-bitcol-nth-set-bound
  (b* ((?nth-row (s32v-bitcol-nth-set row nleft bitcol s32v)))
    (implies (< (nfix row)
                (len (stobjs::2darr->rows s32v)))
             (< nth-row
                (len (stobjs::2darr->rows s32v)))))
  :rule-classes :linear)

Theorem: s32v-bitcol-nth-set-of-nfix-row

(defthm s32v-bitcol-nth-set-of-nfix-row
  (equal (s32v-bitcol-nth-set (nfix row)
                              nleft bitcol s32v)
         (s32v-bitcol-nth-set row nleft bitcol s32v)))

Theorem: s32v-bitcol-nth-set-nat-equiv-congruence-on-row

(defthm s32v-bitcol-nth-set-nat-equiv-congruence-on-row
 (implies (nat-equiv row row-equiv)
          (equal (s32v-bitcol-nth-set row nleft bitcol s32v)
                 (s32v-bitcol-nth-set row-equiv nleft bitcol s32v)))
 :rule-classes :congruence)

Theorem: s32v-bitcol-nth-set-of-nfix-nleft

(defthm s32v-bitcol-nth-set-of-nfix-nleft
  (equal (s32v-bitcol-nth-set row (nfix nleft)
                              bitcol s32v)
         (s32v-bitcol-nth-set row nleft bitcol s32v)))

Theorem: s32v-bitcol-nth-set-nat-equiv-congruence-on-nleft

(defthm s32v-bitcol-nth-set-nat-equiv-congruence-on-nleft
 (implies (nat-equiv nleft nleft-equiv)
          (equal (s32v-bitcol-nth-set row nleft bitcol s32v)
                 (s32v-bitcol-nth-set row nleft-equiv bitcol s32v)))
 :rule-classes :congruence)

Theorem: s32v-bitcol-nth-set-of-nfix-bitcol

(defthm s32v-bitcol-nth-set-of-nfix-bitcol
  (equal (s32v-bitcol-nth-set row nleft (nfix bitcol)
                              s32v)
         (s32v-bitcol-nth-set row nleft bitcol s32v)))

Theorem: s32v-bitcol-nth-set-nat-equiv-congruence-on-bitcol

(defthm s32v-bitcol-nth-set-nat-equiv-congruence-on-bitcol
 (implies (nat-equiv bitcol bitcol-equiv)
          (equal (s32v-bitcol-nth-set row nleft bitcol s32v)
                 (s32v-bitcol-nth-set row nleft bitcol-equiv s32v)))
 :rule-classes :congruence)