		Search-engine friendly clone of the ACL2 documentation.

Obj-declor

Obj-declor-count

Measure for recurring over obj-declor structures.

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

Definitions and Theorems

Function: obj-declor-count

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

Theorem: natp-of-obj-declor-count

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

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

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

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

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

Theorem: obj-declor-count-of-obj-declor-pointer

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

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

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

Theorem: obj-declor-count-of-obj-declor-array

(defthm obj-declor-count-of-obj-declor-array
  (implies t
           (< (+ (obj-declor-count decl))
              (obj-declor-count (obj-declor-array decl size))))
  :rule-classes :linear)

Theorem: obj-declor-count-of-obj-declor-array->decl

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