		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrexes-ok

Signature
(fraig-ctrexes-ok fraig-ctrexes) → ok

Definitions and Theorems

Function: fraig-ctrexes-ok

(defun fraig-ctrexes-ok (fraig-ctrexes)
  (declare (xargs :stobjs (fraig-ctrexes)))
  (declare (xargs :guard t))
  (let ((__function__ 'fraig-ctrexes-ok))
    (declare (ignorable __function__))
    (b* ((nctrexes (lnfix (fraig-ctrex-nbits fraig-ctrexes)))
         ((acl2::stobj-get ncols data-and-resims-ok)
          ((s32v (fraig-ctrex-data fraig-ctrexes))
           (bitarr (fraig-ctrex-resim-classes fraig-ctrexes)))
          (mv (s32v-ncols s32v)
              (equal (s32v-nrows s32v)
                     (bits-length bitarr))))
         ((acl2::stobj-get vals/relevants-ok)
          ((packed-vals (fraig-ctrex-in/reg-vals fraig-ctrexes))
           (packed-relevants
                (fraig-ctrex-in/reg-relevants fraig-ctrexes)))
          (and (equal (s32v-ncols packed-vals) ncols)
               (equal (s32v-ncols packed-relevants)
                      ncols)
               (equal (s32v-nrows packed-vals)
                      (s32v-nrows packed-relevants)))))
      (and (posp ncols)
           (<= nctrexes (* 32 ncols))
           data-and-resims-ok vals/relevants-ok))))

Theorem: fraig-ctrexes-ok-implies-data-rows

(defthm fraig-ctrexes-ok-implies-data-rows
 (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
  (implies
   ok
   (equal
    (len
       (stobjs::2darr->rows (nth *fraig-ctrex-data* fraig-ctrexes)))
    (fraig-ctrex-data-rows fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-data-columns

(defthm fraig-ctrexes-ok-implies-data-columns
 (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
  (implies
   ok
   (equal
       (stobjs::2darr->ncols (nth *fraig-ctrex-data* fraig-ctrexes))
       (fraig-ctrex-ncols fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-classes-len

(defthm fraig-ctrexes-ok-implies-classes-len
  (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
    (implies ok
             (equal (len (nth *fraig-ctrex-resim-classes*
                              fraig-ctrexes))
                    (fraig-ctrex-data-rows fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-vals-rows

(defthm fraig-ctrexes-ok-implies-vals-rows
 (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
  (implies
     ok
     (equal (len (stobjs::2darr->rows (nth *fraig-ctrex-in/reg-vals*
                                           fraig-ctrexes)))
            (fraig-ctrex-in/reg-rows fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-relevants-rows

(defthm fraig-ctrexes-ok-implies-relevants-rows
 (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
  (implies
   ok
   (equal
       (len (stobjs::2darr->rows (nth *fraig-ctrex-in/reg-relevants*
                                      fraig-ctrexes)))
       (fraig-ctrex-in/reg-rows fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-vals-columns

(defthm fraig-ctrexes-ok-implies-vals-columns
  (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
    (implies
         ok
         (equal (stobjs::2darr->ncols (nth *fraig-ctrex-in/reg-vals*
                                           fraig-ctrexes))
                (fraig-ctrex-ncols fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-relevants-columns

(defthm fraig-ctrexes-ok-implies-relevants-columns
 (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
  (implies
    ok
    (equal (stobjs::2darr->ncols (nth *fraig-ctrex-in/reg-relevants*
                                      fraig-ctrexes))
           (fraig-ctrex-ncols fraig-ctrexes)))))

Theorem: fraig-ctrexes-ok-implies-ncols-posp

(defthm fraig-ctrexes-ok-implies-ncols-posp
  (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
    (implies ok
             (posp (fraig-ctrex-ncols fraig-ctrexes))))
  :rule-classes :forward-chaining)

Theorem: fraig-ctrexes-ok-implies-nctrexes-bound

(defthm fraig-ctrexes-ok-implies-nctrexes-bound
  (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
    (implies ok
             (<= (nfix (nth *fraig-ctrex-nbits* fraig-ctrexes))
                 (* 32 (fraig-ctrex-ncols fraig-ctrexes)))))
  :rule-classes :linear)

Theorem: fraig-ctrexes-ok-implies-nctrexes-bound-natp

(defthm fraig-ctrexes-ok-implies-nctrexes-bound-natp
  (b* ((?ok (fraig-ctrexes-ok fraig-ctrexes)))
    (implies (and ok
                  (natp (nth *fraig-ctrex-nbits* fraig-ctrexes)))
             (<= (nth *fraig-ctrex-nbits* fraig-ctrexes)
                 (* 32 (fraig-ctrex-ncols fraig-ctrexes)))))
  :rule-classes :linear)