Function:
(defun vl-hidindex-count-indices (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-hidindex-p x))) (let ((__function__ 'vl-hidindex-count-indices)) (declare (ignorable __function__)) (mbe :logic (len (vl-hidindex->indices x)) :exec (if (vl-atom-p x) 0 (+ 1 (vl-hidindex-count-indices (first (vl-nonatom->args x))))))))
Theorem:
(defthm natp-of-vl-hidindex-count-indices (b* ((idxcount (vl-hidindex-count-indices x))) (natp idxcount)) :rule-classes :type-prescription)
Theorem:
(defthm vl-hidindex-count-indices-of-vl-expr-fix-x (equal (vl-hidindex-count-indices (vl-expr-fix x)) (vl-hidindex-count-indices x)))
Theorem:
(defthm vl-hidindex-count-indices-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-hidindex-count-indices x) (vl-hidindex-count-indices x-equiv))) :rule-classes :congruence)