		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-ok

Signature
(moddb-ok moddb) → *
Arguments: moddb — Guard (moddbp moddb).

Definitions and Theorems

Function: moddb-ok

(defun moddb-ok (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (moddbp moddb)))
  (let ((__function__ 'moddb-ok))
    (declare (ignorable __function__))
    (and (moddb-basics-ok moddb)
         (moddb-mods-ok moddb))))

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

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

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

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