		Search-engine friendly clone of the ACL2 documentation.

Rewriting

Svexlist-count-calls-aux

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

Definitions and Theorems

Function: svexlist-count-calls-aux

(defun svexlist-count-calls-aux (x acc)
  (declare (xargs :guard (and (svexlist-p x) (natp acc))))
  (let ((__function__ 'svexlist-count-calls-aux))
    (declare (ignorable __function__))
    (if (atom x)
        (lnfix acc)
      (svexlist-count-calls-aux
           (cdr x)
           (+ (let ((x1 (car x)))
                (svex-case x1 :call 1 :otherwise 0))
              (lnfix acc))))))

Theorem: natp-of-svexlist-count-calls-aux

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

Theorem: svexlist-count-calls-aux-of-svexlist-fix-x

(defthm svexlist-count-calls-aux-of-svexlist-fix-x
  (equal (svexlist-count-calls-aux (svexlist-fix x)
                                   acc)
         (svexlist-count-calls-aux x acc)))

Theorem: svexlist-count-calls-aux-svexlist-equiv-congruence-on-x

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

Theorem: svexlist-count-calls-aux-of-nfix-acc

(defthm svexlist-count-calls-aux-of-nfix-acc
  (equal (svexlist-count-calls-aux x (nfix acc))
         (svexlist-count-calls-aux x acc)))

Theorem: svexlist-count-calls-aux-nat-equiv-congruence-on-acc

(defthm svexlist-count-calls-aux-nat-equiv-congruence-on-acc
  (implies (nat-equiv acc acc-equiv)
           (equal (svexlist-count-calls-aux x acc)
                  (svexlist-count-calls-aux x acc-equiv)))
  :rule-classes :congruence)