		Search-engine friendly clone of the ACL2 documentation.

Vl-scopeitem

Vl-scopeitem-alist-count

Signature
(vl-scopeitem-alist-count x) → count
Arguments: x — Guard (vl-scopeitem-alist-p x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: vl-scopeitem-alist-count

(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: natp-of-vl-scopeitem-alist-count

(defthm natp-of-vl-scopeitem-alist-count
  (b* ((count (vl-scopeitem-alist-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: vl-scopeitem-alist-count-of-vl-scopeitem-alist-fix-x

(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: vl-scopeitem-alist-count-vl-scopeitem-alist-equiv-congruence-on-x

(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: vl-scopeitem-alist-count-of-cons

(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: vl-scopeitem-alist-count-of-cdr

(defthm vl-scopeitem-alist-count-of-cdr
  (<= (vl-scopeitem-alist-count (cdr x))
      (vl-scopeitem-alist-count x))
  :rule-classes :linear)

Theorem: vl-scopeitem-alist-count-of-cdr-strong

(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)