		Search-engine friendly clone of the ACL2 documentation.

Location

Location-count

Measure for recurring over location structures.

Signature
(location-count x) → count
Arguments: x — Guard (locationp x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: location-count

(defun location-count (x)
 (declare (xargs :guard (locationp x)))
 (let ((__function__ 'location-count))
  (declare (ignorable __function__))
  (case (location-kind x)
   (:var 1)
   (:tuple-comp (+ 3
                   (location-count (location-tuple-comp->tuple x))))
   (:struct-comp
        (+ 3
           (location-count (location-struct-comp->struct x)))))))

Theorem: natp-of-location-count

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

Theorem: location-count-of-location-fix-x

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

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

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

Theorem: location-count-of-location-tuple-comp

(defthm location-count-of-location-tuple-comp
  (implies t
           (< (+ (location-count tuple))
              (location-count (location-tuple-comp tuple index))))
  :rule-classes :linear)

Theorem: location-count-of-location-tuple-comp->tuple

(defthm location-count-of-location-tuple-comp->tuple
  (implies (equal (location-kind x) :tuple-comp)
           (< (location-count (location-tuple-comp->tuple x))
              (location-count x)))
  :rule-classes :linear)

Theorem: location-count-of-location-struct-comp

(defthm location-count-of-location-struct-comp
  (implies t
           (< (+ (location-count struct))
              (location-count (location-struct-comp struct name))))
  :rule-classes :linear)

Theorem: location-count-of-location-struct-comp->struct

(defthm location-count-of-location-struct-comp->struct
  (implies (equal (location-kind x) :struct-comp)
           (< (location-count (location-struct-comp->struct x))
              (location-count x)))
  :rule-classes :linear)