		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-find-bad-mod

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

Definitions and Theorems

Function: moddb-find-bad-mod

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

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

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

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

(defthm moddb-find-bad-mod-of-nfix-n
  (equal (moddb-find-bad-mod (nfix n) moddb)
         (moddb-find-bad-mod n moddb)))

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

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

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

(defthm moddb-find-bad-mod-of-moddb-fix-moddb
  (equal (moddb-find-bad-mod n (moddb-fix moddb))
         (moddb-find-bad-mod n moddb)))

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

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

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

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

Theorem: moddb-find-bad-mod-bound

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

Theorem: moddb-find-bad-mod-nmods-bound

(defthm moddb-find-bad-mod-nmods-bound
  (implies (moddb-find-bad-mod n moddb)
           (< (moddb-find-bad-mod n moddb)
              (nfix (nth *moddb->nmods* moddb))))
  :rule-classes :linear)

Theorem: moddb-find-bad-mod-is-bad

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

Theorem: moddb-find-bad-mod-finds-bad

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