		Search-engine friendly clone of the ACL2 documentation.

Fun-adeclor

Fun-adeclor-count

Measure for recurring over fun-adeclor structures.

Signature
(fun-adeclor-count x) → count
Arguments: x — Guard (fun-adeclorp x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: fun-adeclor-count

(defun fun-adeclor-count (x)
  (declare (xargs :guard (fun-adeclorp x)))
  (let ((__function__ 'fun-adeclor-count))
    (declare (ignorable __function__))
    (case (fun-adeclor-kind x)
      (:base 1)
      (:pointer
           (+ 2
              (fun-adeclor-count (fun-adeclor-pointer->decl x)))))))

Theorem: natp-of-fun-adeclor-count

(defthm natp-of-fun-adeclor-count
  (b* ((count (fun-adeclor-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: fun-adeclor-count-of-fun-adeclor-fix-x

(defthm fun-adeclor-count-of-fun-adeclor-fix-x
  (equal (fun-adeclor-count (fun-adeclor-fix x))
         (fun-adeclor-count x)))

Theorem: fun-adeclor-count-fun-adeclor-equiv-congruence-on-x

(defthm fun-adeclor-count-fun-adeclor-equiv-congruence-on-x
  (implies (fun-adeclor-equiv x x-equiv)
           (equal (fun-adeclor-count x)
                  (fun-adeclor-count x-equiv)))
  :rule-classes :congruence)

Theorem: fun-adeclor-count-of-fun-adeclor-pointer

(defthm fun-adeclor-count-of-fun-adeclor-pointer
  (implies t
           (< (+ (fun-adeclor-count decl))
              (fun-adeclor-count (fun-adeclor-pointer decl))))
  :rule-classes :linear)

Theorem: fun-adeclor-count-of-fun-adeclor-pointer->decl

(defthm fun-adeclor-count-of-fun-adeclor-pointer->decl
  (implies (equal (fun-adeclor-kind x) :pointer)
           (< (fun-adeclor-count (fun-adeclor-pointer->decl x))
              (fun-adeclor-count x)))
  :rule-classes :linear)