		Search-engine friendly clone of the ACL2 documentation.

Modscope

Modscope-count

Measure for recurring over modscope structures.

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

Definitions and Theorems

Function: modscope-count

(defun modscope-count (x)
  (declare (xargs :guard (modscope-p x)))
  (let ((__function__ 'modscope-count))
    (declare (ignorable __function__))
    (case (modscope-kind x)
      (:top 1)
      (:nested (+ 5
                  (modscope-count (modscope-nested->upper x)))))))

Theorem: natp-of-modscope-count

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

Theorem: modscope-count-of-modscope-fix-x

(defthm modscope-count-of-modscope-fix-x
  (equal (modscope-count (modscope-fix x))
         (modscope-count x)))

Theorem: modscope-count-modscope-equiv-congruence-on-x

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

Theorem: modscope-count-of-modscope-nested

(defthm modscope-count-of-modscope-nested
 (implies
     t
     (< (+ (modscope-count upper))
        (modscope-count
             (modscope-nested modidx wireoffset instoffset upper))))
 :rule-classes :linear)

Theorem: modscope-count-of-modscope-nested->upper

(defthm modscope-count-of-modscope-nested->upper
  (implies (equal (modscope-kind x) :nested)
           (< (modscope-count (modscope-nested->upper x))
              (modscope-count x)))
  :rule-classes :linear)