		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-find-bad-modinst

Signature
(moddb-find-bad-modinst n modidx moddb) → idx
Arguments: n — Guard (natp n).; modidx — Guard (natp modidx).
Returns: idx — Type (iff (natp idx) idx).

Definitions and Theorems

Function: moddb-find-bad-modinst

(defun moddb-find-bad-modinst (n modidx moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (natp n) (natp modidx))))
 (declare
  (xargs
     :guard (and (< modidx (moddb->nmods moddb))
                 (<= (moddb->nmods moddb)
                     (moddb->mods-length moddb))
                 (moddb-mod-order-ok modidx moddb)
                 (stobj-let ((elab-mod (moddb->modsi modidx moddb)))
                            (ok)
                            (<= n (elab-mod-ninsts elab-mod))
                            ok))))
 (let ((__function__ 'moddb-find-bad-modinst))
   (declare (ignorable __function__))
   (if (zp n)
       nil
     (if (moddb-modinst-ok (1- n) modidx moddb)
         (moddb-find-bad-modinst (1- n)
                                 modidx moddb)
       (1- n)))))

Theorem: return-type-of-moddb-find-bad-modinst

(defthm return-type-of-moddb-find-bad-modinst
  (b* ((idx (moddb-find-bad-modinst n modidx moddb)))
    (iff (natp idx) idx))
  :rule-classes :rewrite)

Theorem: moddb-find-bad-modinst-of-nfix-n

(defthm moddb-find-bad-modinst-of-nfix-n
  (equal (moddb-find-bad-modinst (nfix n)
                                 modidx moddb)
         (moddb-find-bad-modinst n modidx moddb)))

Theorem: moddb-find-bad-modinst-nat-equiv-congruence-on-n

(defthm moddb-find-bad-modinst-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (moddb-find-bad-modinst n modidx moddb)
                  (moddb-find-bad-modinst n-equiv modidx moddb)))
  :rule-classes :congruence)

Theorem: moddb-find-bad-modinst-of-nfix-modidx

(defthm moddb-find-bad-modinst-of-nfix-modidx
  (equal (moddb-find-bad-modinst n (nfix modidx)
                                 moddb)
         (moddb-find-bad-modinst n modidx moddb)))

Theorem: moddb-find-bad-modinst-nat-equiv-congruence-on-modidx

(defthm moddb-find-bad-modinst-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (moddb-find-bad-modinst n modidx moddb)
                  (moddb-find-bad-modinst n modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-find-bad-modinst-of-moddb-fix-moddb

(defthm moddb-find-bad-modinst-of-moddb-fix-moddb
  (equal (moddb-find-bad-modinst n modidx (moddb-fix moddb))
         (moddb-find-bad-modinst n modidx moddb)))

Theorem: moddb-find-bad-modinst-moddb-equiv-congruence-on-moddb

(defthm moddb-find-bad-modinst-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-find-bad-modinst n modidx moddb)
                  (moddb-find-bad-modinst n modidx moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-find-bad-modinst-bound-weak

(defthm moddb-find-bad-modinst-bound-weak
  (<= (moddb-find-bad-modinst n modidx moddb)
      (nfix n))
  :rule-classes :linear)

Theorem: moddb-find-bad-modinst-bound

(defthm moddb-find-bad-modinst-bound
  (implies (moddb-find-bad-modinst n modidx moddb)
           (< (moddb-find-bad-modinst n modidx moddb)
              (nfix n)))
  :rule-classes :linear)

Theorem: moddb-find-bad-modinst-is-bad

(defthm moddb-find-bad-modinst-is-bad
 (implies
      (moddb-find-bad-modinst n modidx moddb)
      (not (moddb-modinst-ok (moddb-find-bad-modinst n modidx moddb)
                             modidx moddb))))

Theorem: moddb-find-bad-modinst-finds-bad

(defthm moddb-find-bad-modinst-finds-bad
 (implies
  (and (not (moddb-modinst-ok idx modidx moddb))
       (< (nfix idx) (nfix n)))
  (and
      (moddb-find-bad-modinst n modidx moddb)
      (not (moddb-modinst-ok (moddb-find-bad-modinst n modidx moddb)
                             modidx moddb)))))