Measure for recurring over jtype structures.
Function:
(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:
(defthm natp-of-jtype-count (b* ((count (jtype-count x))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm jtype-count-of-jtype-fix-x (equal (jtype-count (jtype-fix x)) (jtype-count x)))
Theorem:
(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:
(defthm jtype-count-of-jtype-array (implies t (< (+ (jtype-count comp)) (jtype-count (jtype-array comp)))) :rule-classes :linear)
Theorem:
(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)