		Search-engine friendly clone of the ACL2 documentation.

Value

Value-count

Measure for recurring over value structures.

Signature
(value-count x) → count
Arguments: x — Guard (valuep x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: value-count

(defun value-count (x)
  (declare (xargs :guard (valuep x)))
  (let ((__function__ 'value-count))
    (declare (ignorable __function__))
    (case (value-kind x)
      (:number 1)
      (:character 1)
      (:string 1)
      (:symbol 1)
      (:cons (+ 3 (value-count (value-cons->car x))
                (value-count (value-cons->cdr x)))))))

Theorem: natp-of-value-count

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

Theorem: value-count-of-value-fix-x

(defthm value-count-of-value-fix-x
  (equal (value-count (value-fix x))
         (value-count x)))

Theorem: value-count-value-equiv-congruence-on-x

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

Theorem: value-count-of-value-cons

(defthm value-count-of-value-cons
  (implies t
           (< (+ (value-count car) (value-count cdr))
              (value-count (value-cons car cdr))))
  :rule-classes :linear)

Theorem: value-count-of-value-cons->car

(defthm value-count-of-value-cons->car
  (implies (equal (value-kind x) :cons)
           (< (value-count (value-cons->car x))
              (value-count x)))
  :rule-classes :linear)

Theorem: value-count-of-value-cons->cdr

(defthm value-count-of-value-cons->cdr
  (implies (equal (value-kind x) :cons)
           (< (value-count (value-cons->cdr x))
              (value-count x)))
  :rule-classes :linear)