		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svex-named->indexed-memo-ok

Signature
(svex-named->indexed-memo-ok x modidx moddb) → *
Arguments: x — Guard (svex-p x).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: svex-named->indexed-memo-ok$inline

(defun svex-named->indexed-memo-ok$inline (x modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (svex-p x)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare (xargs :guard (and (svarlist-addr-p (svex-vars x))
                              (< modidx (moddb->nmods moddb)))))
  (let ((__function__ 'svex-named->indexed-memo-ok))
    (declare (ignorable __function__))
    (eq (svex-kind x) :call)))

Theorem: svex-named->indexed-memo-ok$inline-of-svex-fix-x

(defthm svex-named->indexed-memo-ok$inline-of-svex-fix-x
  (equal (svex-named->indexed-memo-ok$inline (svex-fix x)
                                             modidx moddb)
         (svex-named->indexed-memo-ok$inline x modidx moddb)))

Theorem: svex-named->indexed-memo-ok$inline-svex-equiv-congruence-on-x

(defthm
      svex-named->indexed-memo-ok$inline-svex-equiv-congruence-on-x
 (implies
  (svex-equiv x x-equiv)
  (equal (svex-named->indexed-memo-ok$inline x modidx moddb)
         (svex-named->indexed-memo-ok$inline x-equiv modidx moddb)))
 :rule-classes :congruence)

Theorem: svex-named->indexed-memo-ok$inline-of-nfix-modidx

(defthm svex-named->indexed-memo-ok$inline-of-nfix-modidx
  (equal (svex-named->indexed-memo-ok$inline x (nfix modidx)
                                             moddb)
         (svex-named->indexed-memo-ok$inline x modidx moddb)))

Theorem: svex-named->indexed-memo-ok$inline-nat-equiv-congruence-on-modidx

(defthm
  svex-named->indexed-memo-ok$inline-nat-equiv-congruence-on-modidx
 (implies
  (nat-equiv modidx modidx-equiv)
  (equal (svex-named->indexed-memo-ok$inline x modidx moddb)
         (svex-named->indexed-memo-ok$inline x modidx-equiv moddb)))
 :rule-classes :congruence)

Theorem: svex-named->indexed-memo-ok$inline-of-moddb-fix-moddb

(defthm svex-named->indexed-memo-ok$inline-of-moddb-fix-moddb
 (equal
     (svex-named->indexed-memo-ok$inline x modidx (moddb-fix moddb))
     (svex-named->indexed-memo-ok$inline x modidx moddb)))

Theorem: svex-named->indexed-memo-ok$inline-moddb-equiv-congruence-on-moddb

(defthm
 svex-named->indexed-memo-ok$inline-moddb-equiv-congruence-on-moddb
 (implies
  (moddb-equiv moddb moddb-equiv)
  (equal (svex-named->indexed-memo-ok$inline x modidx moddb)
         (svex-named->indexed-memo-ok$inline x modidx moddb-equiv)))
 :rule-classes :congruence)