		Search-engine friendly clone of the ACL2 documentation.

Fun-declor

Fun-declor-count

Measure for recurring over fun-declor structures.

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

Definitions and Theorems

Function: fun-declor-count

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

Theorem: natp-of-fun-declor-count

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

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

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

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

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

Theorem: fun-declor-count-of-fun-declor-pointer

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

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

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