		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope-local-bound

Signature
(modscope-local-bound scope moddb) → *
Arguments: scope — Guard (modscope-p scope).; moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: modscope-local-bound

(defun modscope-local-bound (scope moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (modscope-p scope)
                              (moddb-ok moddb))))
  (declare (xargs :guard (modscope-okp scope moddb)))
  (let ((__function__ 'modscope-local-bound))
    (declare (ignorable __function__))
    (moddb-mod-totalwires (modscope->modidx scope)
                          moddb)))

Theorem: modscope-local-bound-of-modscope-fix-scope

(defthm modscope-local-bound-of-modscope-fix-scope
  (equal (modscope-local-bound (modscope-fix scope)
                               moddb)
         (modscope-local-bound scope moddb)))

Theorem: modscope-local-bound-modscope-equiv-congruence-on-scope

(defthm modscope-local-bound-modscope-equiv-congruence-on-scope
  (implies (modscope-equiv scope scope-equiv)
           (equal (modscope-local-bound scope moddb)
                  (modscope-local-bound scope-equiv moddb)))
  :rule-classes :congruence)

Theorem: modscope-local-bound-of-moddb-fix-moddb

(defthm modscope-local-bound-of-moddb-fix-moddb
  (equal (modscope-local-bound scope (moddb-fix moddb))
         (modscope-local-bound scope moddb)))

Theorem: modscope-local-bound-moddb-equiv-congruence-on-moddb

(defthm modscope-local-bound-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (modscope-local-bound scope moddb)
                  (modscope-local-bound scope moddb-equiv)))
  :rule-classes :congruence)