		Search-engine friendly clone of the ACL2 documentation.

Svar-split

Svar-split-count

Measure for recurring over svar-split structures.

Signature
(svar-split-count x) → count
Arguments: x — Guard (svar-split-p x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: svar-split-count

(defun svar-split-count (x)
  (declare (xargs :guard (svar-split-p x)))
  (let ((__function__ 'svar-split-count))
    (declare (ignorable __function__))
    (case (svar-split-kind x)
      (:segment (+ 4
                   (svar-split-count (svar-split-segment->rest x))))
      (:remainder 1))))

Theorem: natp-of-svar-split-count

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

Theorem: svar-split-count-of-svar-split-fix-x

(defthm svar-split-count-of-svar-split-fix-x
  (equal (svar-split-count (svar-split-fix x))
         (svar-split-count x)))

Theorem: svar-split-count-svar-split-equiv-congruence-on-x

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

Theorem: svar-split-count-of-svar-split-segment

(defthm svar-split-count-of-svar-split-segment
  (implies
       t
       (< (+ (svar-split-count rest))
          (svar-split-count (svar-split-segment width var rest))))
  :rule-classes :linear)

Theorem: svar-split-count-of-svar-split-segment->rest

(defthm svar-split-count-of-svar-split-segment->rest
  (implies (equal (svar-split-kind x) :segment)
           (< (svar-split-count (svar-split-segment->rest x))
              (svar-split-count x)))
  :rule-classes :linear)