		Search-engine friendly clone of the ACL2 documentation.

Jtype

Jtype-count

Measure for recurring over jtype structures.

Signature
(jtype-count x) → count
Arguments: x — Guard (jtypep x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: jtype-count

(defun jtype-count (x)
  (declare (xargs :guard (jtypep x)))
  (let ((__function__ 'jtype-count))
    (declare (ignorable __function__))
    (case (jtype-kind x)
      (:prim 1)
      (:class 1)
      (:array (+ 2
                 (jtype-count (jtype-array->comp x)))))))

Theorem: natp-of-jtype-count

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

Theorem: jtype-count-of-jtype-fix-x

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

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

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

Theorem: jtype-count-of-jtype-array

(defthm jtype-count-of-jtype-array
  (implies t
           (< (+ (jtype-count comp))
              (jtype-count (jtype-array comp))))
  :rule-classes :linear)

Theorem: jtype-count-of-jtype-array->comp

(defthm jtype-count-of-jtype-array->comp
  (implies (equal (jtype-kind x) :array)
           (< (jtype-count (jtype-array->comp x))
              (jtype-count x)))
  :rule-classes :linear)