		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svex->absindexed-memo-ok

Signature
(svex->absindexed-memo-ok x scope moddb) → *
Arguments: x — Guard (svex-p x).; scope — Guard (modscope-p scope).; moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: svex->absindexed-memo-ok$inline

(defun svex->absindexed-memo-ok$inline (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (svex-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (svex-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'svex->absindexed-memo-ok))
   (declare (ignorable __function__))
   (eq (svex-kind x) :call)))

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

(defthm svex->absindexed-memo-ok$inline-of-svex-fix-x
  (equal (svex->absindexed-memo-ok$inline (svex-fix x)
                                          scope moddb)
         (svex->absindexed-memo-ok$inline x scope moddb)))

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

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

Theorem: svex->absindexed-memo-ok$inline-of-modscope-fix-scope

(defthm svex->absindexed-memo-ok$inline-of-modscope-fix-scope
  (equal (svex->absindexed-memo-ok$inline x (modscope-fix scope)
                                          moddb)
         (svex->absindexed-memo-ok$inline x scope moddb)))

Theorem: svex->absindexed-memo-ok$inline-modscope-equiv-congruence-on-scope

(defthm
 svex->absindexed-memo-ok$inline-modscope-equiv-congruence-on-scope
 (implies
      (modscope-equiv scope scope-equiv)
      (equal (svex->absindexed-memo-ok$inline x scope moddb)
             (svex->absindexed-memo-ok$inline x scope-equiv moddb)))
 :rule-classes :congruence)

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

(defthm svex->absindexed-memo-ok$inline-of-moddb-fix-moddb
  (equal (svex->absindexed-memo-ok$inline x scope (moddb-fix moddb))
         (svex->absindexed-memo-ok$inline x scope moddb)))

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

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