		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope->instoffset

Signature
(modscope->instoffset x) → instoffset
Arguments: x — Guard (modscope-p x).
Returns: instoffset — Type (natp instoffset).

Definitions and Theorems

Function: modscope->instoffset

(defun modscope->instoffset (x)
  (declare (xargs :guard (modscope-p x)))
  (let ((__function__ 'modscope->instoffset))
    (declare (ignorable __function__))
    (modscope-case x
                   :top 0
                   :nested x.instoffset)))

Theorem: natp-of-modscope->instoffset

(defthm natp-of-modscope->instoffset
  (b* ((instoffset (modscope->instoffset x)))
    (natp instoffset))
  :rule-classes :type-prescription)

Theorem: modscope->instoffset-of-modscope-fix-x

(defthm modscope->instoffset-of-modscope-fix-x
  (equal (modscope->instoffset (modscope-fix x))
         (modscope->instoffset x)))

Theorem: modscope->instoffset-modscope-equiv-congruence-on-x

(defthm modscope->instoffset-modscope-equiv-congruence-on-x
  (implies (modscope-equiv x x-equiv)
           (equal (modscope->instoffset x)
                  (modscope->instoffset x-equiv)))
  :rule-classes :congruence)