		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Moddb-basics-ok

Signature
(moddb-basics-ok moddb) → *

Definitions and Theorems

Function: moddb-basics-ok

(defun moddb-basics-ok (moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard t))
  (let ((__function__ 'moddb-basics-ok))
    (declare (ignorable __function__))
    (and (<= (lnfix (moddb->nmods moddb))
             (moddb->mods-length moddb))
         (eql (lnfix (moddb->nmods moddb))
              (moddb->modname-idxes-count moddb))
         (moddb-indices-ok moddb))))

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

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

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

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

Theorem: moddb-basics-linear

(defthm moddb-basics-linear
  (implies (moddb-basics-ok moddb)
           (<= (nfix (nth *moddb->nmods* moddb))
               (len (nth *moddb->modsi* moddb))))
  :rule-classes :linear)

Theorem: moddb-basics-count

(defthm moddb-basics-count
  (implies (moddb-basics-ok moddb)
           (eql (count-keys (nth *moddb->modname-idxes-get* moddb))
                (lnfix (moddb->nmods moddb)))))

Theorem: moddb-indices-ok-when-moddb-basics-ok

(defthm moddb-indices-ok-when-moddb-basics-ok
  (implies (moddb-basics-ok moddb)
           (moddb-indices-ok moddb)))

Theorem: moddb-basics-ok-of-norm

(defthm moddb-basics-ok-of-norm
  (implies (moddb-basics-ok moddb)
           (moddb-basics-ok (moddb-norm moddb))))

Theorem: lookup-name-in-moddb-norm

(defthm lookup-name-in-moddb-norm
 (implies
   (moddb-basics-ok moddb)
   (equal
        (hons-assoc-equal name
                          (nth *moddb->modname-idxes-get*
                               (moddb-norm moddb)))
        (hons-assoc-equal name
                          (nth *moddb->modname-idxes-get* moddb)))))