		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope-top-bound

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

Definitions and Theorems

Function: modscope-top-bound

(defun modscope-top-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-top-bound))
    (declare (ignorable __function__))
    (moddb-mod-totalwires (modscope->modidx (modscope->top scope))
                          moddb)))

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

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

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

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

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

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

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

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