		Search-engine friendly clone of the ACL2 documentation.

Name-database

Vl-namedb-pmap-okp

Signature
(vl-namedb-pmap-okp names pmap) → *
Arguments: names — Guard (vl-namedb-nameset-p names).; pmap — Guard (vl-namedb-prefixmap-p pmap).

Definitions and Theorems

Function: vl-namedb-pmap-okp

(defun vl-namedb-pmap-okp (names pmap)
  (declare (xargs :guard (and (vl-namedb-nameset-p names)
                              (vl-namedb-prefixmap-p pmap))))
  (let ((__function__ 'vl-namedb-pmap-okp))
    (declare (ignorable __function__))
    (b* ((names (vl-namedb-nameset-fix names))
         (pmap (vl-namedb-prefixmap-fix pmap)))
      (vl-prefix-map-correct-p pmap (alist-keys names)))))

Theorem: vl-namedb-pmap-okp-of-nil

(defthm vl-namedb-pmap-okp-of-nil
  (implies (not pmap)
           (vl-namedb-pmap-okp names pmap)))

Theorem: vl-namedb-pmap-okp-of-vl-namedb-nameset-fix-names

(defthm vl-namedb-pmap-okp-of-vl-namedb-nameset-fix-names
  (equal (vl-namedb-pmap-okp (vl-namedb-nameset-fix names)
                             pmap)
         (vl-namedb-pmap-okp names pmap)))

Theorem: vl-namedb-pmap-okp-vl-namedb-nameset-equiv-congruence-on-names

(defthm
     vl-namedb-pmap-okp-vl-namedb-nameset-equiv-congruence-on-names
  (implies (vl-namedb-nameset-equiv names names-equiv)
           (equal (vl-namedb-pmap-okp names pmap)
                  (vl-namedb-pmap-okp names-equiv pmap)))
  :rule-classes :congruence)

Theorem: vl-namedb-pmap-okp-of-vl-namedb-prefixmap-fix-pmap

(defthm vl-namedb-pmap-okp-of-vl-namedb-prefixmap-fix-pmap
  (equal (vl-namedb-pmap-okp names (vl-namedb-prefixmap-fix pmap))
         (vl-namedb-pmap-okp names pmap)))

Theorem: vl-namedb-pmap-okp-vl-namedb-prefixmap-equiv-congruence-on-pmap

(defthm
    vl-namedb-pmap-okp-vl-namedb-prefixmap-equiv-congruence-on-pmap
  (implies (vl-namedb-prefixmap-equiv pmap pmap-equiv)
           (equal (vl-namedb-pmap-okp names pmap)
                  (vl-namedb-pmap-okp names pmap-equiv)))
  :rule-classes :congruence)