		Search-engine friendly clone of the ACL2 documentation.

Objdesign

Objdesign-count

Measure for recurring over objdesign structures.

Signature
(objdesign-count x) → count
Arguments: x — Guard (objdesignp x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: objdesign-count

(defun objdesign-count (x)
  (declare (xargs :guard (objdesignp x)))
  (let ((__function__ 'objdesign-count))
    (declare (ignorable __function__))
    (case (objdesign-kind x)
      (:static 1)
      (:auto 1)
      (:alloc 1)
      (:element (+ 3
                   (objdesign-count (objdesign-element->super x))))
      (:member (+ 3
                  (objdesign-count (objdesign-member->super x)))))))

Theorem: natp-of-objdesign-count

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

Theorem: objdesign-count-of-objdesign-fix-x

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

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

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

Theorem: objdesign-count-of-objdesign-element

(defthm objdesign-count-of-objdesign-element
  (implies t
           (< (+ (objdesign-count super))
              (objdesign-count (objdesign-element super index))))
  :rule-classes :linear)

Theorem: objdesign-count-of-objdesign-element->super

(defthm objdesign-count-of-objdesign-element->super
  (implies (equal (objdesign-kind x) :element)
           (< (objdesign-count (objdesign-element->super x))
              (objdesign-count x)))
  :rule-classes :linear)

Theorem: objdesign-count-of-objdesign-member

(defthm objdesign-count-of-objdesign-member
  (implies t
           (< (+ (objdesign-count super))
              (objdesign-count (objdesign-member super name))))
  :rule-classes :linear)

Theorem: objdesign-count-of-objdesign-member->super

(defthm objdesign-count-of-objdesign-member->super
  (implies (equal (objdesign-kind x) :member)
           (< (objdesign-count (objdesign-member->super x))
              (objdesign-count x)))
  :rule-classes :linear)