		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-contains-modnames

Signature
(moddb-contains-modnames x moddb) → *
Arguments: x — Guard (modnamelist-p x).; moddb — Guard (moddb-basics-ok moddb).

Definitions and Theorems

Function: moddb-contains-modnames

(defun moddb-contains-modnames (x moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (modnamelist-p x)
                              (moddb-basics-ok moddb))))
  (let ((__function__ 'moddb-contains-modnames))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (moddb-modname-get-index (car x) moddb)
           (moddb-contains-modnames (cdr x)
                                    moddb)))))

Theorem: moddb-contains-modnames-of-modnamelist-fix-x

(defthm moddb-contains-modnames-of-modnamelist-fix-x
  (equal (moddb-contains-modnames (modnamelist-fix x)
                                  moddb)
         (moddb-contains-modnames x moddb)))

Theorem: moddb-contains-modnames-modnamelist-equiv-congruence-on-x

(defthm moddb-contains-modnames-modnamelist-equiv-congruence-on-x
  (implies (modnamelist-equiv x x-equiv)
           (equal (moddb-contains-modnames x moddb)
                  (moddb-contains-modnames x-equiv moddb)))
  :rule-classes :congruence)

Theorem: moddb-contains-modnames-of-moddb-fix-moddb

(defthm moddb-contains-modnames-of-moddb-fix-moddb
  (equal (moddb-contains-modnames x (moddb-fix moddb))
         (moddb-contains-modnames x moddb)))

Theorem: moddb-contains-modnames-moddb-equiv-congruence-on-moddb

(defthm moddb-contains-modnames-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (moddb-contains-modnames x moddb)
                  (moddb-contains-modnames x moddb-equiv)))
  :rule-classes :congruence)