		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-modinst-badguy

Signature
(moddb-modinst-badguy modidx moddb) → *
Arguments: modidx — Guard (natp modidx).

Definitions and Theorems

Function: moddb-modinst-badguy

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

Theorem: moddb-modinst-badguy-of-nfix-modidx

(defthm moddb-modinst-badguy-of-nfix-modidx
  (equal (moddb-modinst-badguy (nfix modidx)
                               moddb)
         (moddb-modinst-badguy modidx moddb)))

Theorem: moddb-modinst-badguy-nat-equiv-congruence-on-modidx

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

Theorem: moddb-modinst-badguy-of-moddb-fix-moddb

(defthm moddb-modinst-badguy-of-moddb-fix-moddb
  (equal (moddb-modinst-badguy modidx (moddb-fix moddb))
         (moddb-modinst-badguy modidx moddb)))

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

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

Theorem: moddb-mod-insts-not-ok

(defthm moddb-mod-insts-not-ok
 (implies
  (acl2::rewriting-positive-literal
       (cons 'moddb-mod-insts-ok
             (cons modidx (cons moddb 'nil))))
  (equal
   (moddb-mod-insts-ok modidx moddb)
   (let ((idx (moddb-modinst-badguy modidx moddb)))
    (or
     (>=
        (nfix idx)
        (elab-mod$a-ninsts (nth modidx (nth *moddb->modsi* moddb))))
     (>= (nfix modidx)
         (nfix (nth *moddb->nmods* moddb)))
     (moddb-modinst-ok idx modidx moddb))))))