		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Modscope->nth

Given some modscope, pop out n frames.

Signature
(modscope->nth n x) → top
Arguments: n — Guard (natp n).; x — Guard (modscope-p x).
Returns: top — Type (modscope-p top).

Definitions and Theorems

Function: modscope->nth

(defun modscope->nth (n x)
  (declare (xargs :guard (and (natp n) (modscope-p x))))
  (let ((__function__ 'modscope->nth))
    (declare (ignorable __function__))
    (if (zp n)
        (modscope-fix x)
      (modscope-case x
                     :top (modscope-fix x)
                     :nested (modscope->nth (1- n) x.upper)))))

Theorem: modscope-p-of-modscope->nth

(defthm modscope-p-of-modscope->nth
  (b* ((top (modscope->nth n x)))
    (modscope-p top))
  :rule-classes :rewrite)

Theorem: modscope-okp-of-modscope->nth

(defthm modscope-okp-of-modscope->nth
  (implies (modscope-okp x moddb)
           (modscope-okp (modscope->nth n x)
                         moddb)))

Theorem: modscope->top-of-nth

(defthm modscope->top-of-nth
  (equal (modscope->top (modscope->nth n x))
         (modscope->top x)))

Theorem: modscope-okp-nth-wireoffset-lower-bound

(defthm modscope-okp-nth-wireoffset-lower-bound
  (implies (modscope-okp x moddb)
           (<= (modscope->wireoffset (modscope->top x))
               (modscope->wireoffset (modscope->nth n x))))
  :rule-classes (:rewrite :linear))

Theorem: modscope-okp-nth-wireidx-bound

(defthm modscope-okp-nth-wireidx-bound
 (implies
  (and (modscope-okp x moddb)
       (moddb-ok moddb))
  (<=
     (+ (modscope->wireoffset (modscope->nth n x))
        (moddb-mod-totalwires (modscope->modidx (modscope->nth n x))
                              moddb))
     (moddb-mod-totalwires (modscope->modidx (modscope->top x))
                           moddb)))
 :rule-classes (:rewrite :linear))

Theorem: modscope->nth-of-nfix-n

(defthm modscope->nth-of-nfix-n
  (equal (modscope->nth (nfix n) x)
         (modscope->nth n x)))

Theorem: modscope->nth-nat-equiv-congruence-on-n

(defthm modscope->nth-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (modscope->nth n x)
                  (modscope->nth n-equiv x)))
  :rule-classes :congruence)

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

(defthm modscope->nth-of-modscope-fix-x
  (equal (modscope->nth n (modscope-fix x))
         (modscope->nth n x)))

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

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