		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-count-calls

Signature
(svexlist-count-calls x) → call-count
Arguments: x — Guard (svexlist-p x).
Returns: call-count — Type (natp call-count).

Definitions and Theorems

Function: svexlist-count-calls$inline

(defun svexlist-count-calls$inline (x)
  (declare (xargs :guard (svexlist-p x)))
  (let ((__function__ 'svexlist-count-calls))
    (declare (ignorable __function__))
    (svexlist-count-calls-aux x 0)))

Theorem: natp-of-svexlist-count-calls

(defthm natp-of-svexlist-count-calls
  (b* ((call-count (svexlist-count-calls$inline x)))
    (natp call-count))
  :rule-classes :type-prescription)

Theorem: svexlist-count-calls$inline-of-svexlist-fix-x

(defthm svexlist-count-calls$inline-of-svexlist-fix-x
  (equal (svexlist-count-calls$inline (svexlist-fix x))
         (svexlist-count-calls$inline x)))

Theorem: svexlist-count-calls$inline-svexlist-equiv-congruence-on-x

(defthm svexlist-count-calls$inline-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlist-count-calls$inline x)
                  (svexlist-count-calls$inline x-equiv)))
  :rule-classes :congruence)