(vl-scopeitem-alist-count x) → count
Function:
(defun vl-scopeitem-alist-count (x) (declare (xargs :guard (vl-scopeitem-alist-p x))) (let ((__function__ 'vl-scopeitem-alist-count)) (declare (ignorable __function__)) (let ((x (mbe :logic (vl-scopeitem-alist-fix x) :exec x))) (if (atom x) 1 (+ 1 (vl-scopeitem-alist-count (cdr x)))))))
Theorem:
(defthm natp-of-vl-scopeitem-alist-count (b* ((count (vl-scopeitem-alist-count x))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm vl-scopeitem-alist-count-of-vl-scopeitem-alist-fix-x (equal (vl-scopeitem-alist-count (vl-scopeitem-alist-fix x)) (vl-scopeitem-alist-count x)))
Theorem:
(defthm vl-scopeitem-alist-count-vl-scopeitem-alist-equiv-congruence-on-x (implies (vl-scopeitem-alist-equiv x x-equiv) (equal (vl-scopeitem-alist-count x) (vl-scopeitem-alist-count x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-scopeitem-alist-count-of-cons (>= (vl-scopeitem-alist-count (cons acl2::a acl2::b)) (vl-scopeitem-alist-count acl2::b)) :rule-classes :linear)
Theorem:
(defthm vl-scopeitem-alist-count-of-cdr (<= (vl-scopeitem-alist-count (cdr x)) (vl-scopeitem-alist-count x)) :rule-classes :linear)
Theorem:
(defthm vl-scopeitem-alist-count-of-cdr-strong (implies (and (vl-scopeitem-alist-p x) (consp x)) (< (vl-scopeitem-alist-count (cdr x)) (vl-scopeitem-alist-count x))) :rule-classes :linear)