		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-mods-ok

Signature
(moddb-mods-ok moddb) → *

Definitions and Theorems

Function: moddb-mods-ok

(defun moddb-mods-ok (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (<= (moddb->nmods moddb)
                             (moddb->mods-length moddb))))
  (let ((__function__ 'moddb-mods-ok))
    (declare (ignorable __function__))
    (not (moddb-find-bad-mod (moddb->nmods moddb)
                             moddb))))

Theorem: moddb-mods-ok-of-moddb-fix-moddb

(defthm moddb-mods-ok-of-moddb-fix-moddb
  (equal (moddb-mods-ok (moddb-fix moddb))
         (moddb-mods-ok moddb)))

Theorem: moddb-mods-ok-moddb-equiv-congruence-on-moddb

(defthm moddb-mods-ok-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-mods-ok moddb)
                  (moddb-mods-ok moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-mods-ok-implies

(defthm moddb-mods-ok-implies
  (implies (moddb-mods-ok moddb)
           (moddb-mod-ok idx moddb)))

Function: moddb-mod-badguy

(defun moddb-mod-badguy (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (prog2$ (acl2::throw-nonexec-error 'moddb-mod-badguy
                                     (list moddb))
          (let ((__function__ 'moddb-mod-badguy))
            (declare (ignorable __function__))
            (let ((moddb (moddb-fix moddb)))
              (moddb-find-bad-mod (moddb->nmods moddb)
                                  moddb)))))

Theorem: moddb-mod-badguy-of-moddb-fix-moddb

(defthm moddb-mod-badguy-of-moddb-fix-moddb
  (equal (moddb-mod-badguy (moddb-fix moddb))
         (moddb-mod-badguy moddb)))

Theorem: moddb-mod-badguy-moddb-equiv-congruence-on-moddb

(defthm moddb-mod-badguy-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-mod-badguy moddb)
                  (moddb-mod-badguy moddb-equiv)))
  :rule-classes :congruence)

Theorem: moddb-mods-not-ok

(defthm moddb-mods-not-ok
  (implies (acl2::rewriting-positive-literal
                (cons 'moddb-mods-ok (cons moddb 'nil)))
           (equal (moddb-mods-ok moddb)
                  (let ((idx (moddb-mod-badguy moddb)))
                    (or (>= (nfix idx)
                            (nfix (nth *moddb->nmods* moddb)))
                        (moddb-mod-ok idx moddb))))))

Theorem: moddb-mods-ok-of-moddb-norm-moddb

(defthm moddb-mods-ok-of-moddb-norm-moddb
  (equal (moddb-mods-ok (moddb-norm moddb))
         (moddb-mods-ok moddb)))

Theorem: moddb-mods-ok-moddb-norm-equiv-congruence-on-moddb

(defthm moddb-mods-ok-moddb-norm-equiv-congruence-on-moddb
  (implies (moddb-norm-equiv moddb moddb-equiv)
           (equal (moddb-mods-ok moddb)
                  (moddb-mods-ok moddb-equiv)))
  :rule-classes :congruence)