		Search-engine friendly clone of the ACL2 documentation.

Rlp-error

Rlp-error-count

Measure for recurring over rlp-error structures.

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

Definitions and Theorems

Function: rlp-error-count

(defun rlp-error-count (x)
  (declare (xargs :guard (rlp-error-p x)))
  (let ((__function__ 'rlp-error-count))
    (declare (ignorable __function__))
    (case (rlp-error-kind x)
      (:no-bytes 1)
      (:fewer-bytes-than-short-length 1)
      (:fewer-bytes-than-length-of-length 1)
      (:fewer-bytes-than-long-length 1)
      (:leading-zeros-in-long-length 1)
      (:non-optimal-short-length 1)
      (:non-optimal-long-length 1)
      (:subtree (+ 2
                   (rlp-error-count (rlp-error-subtree->error x))))
      (:extra-bytes 1)
      (:branch-tree 1)
      (:leading-zeros-in-scalar 1))))

Theorem: natp-of-rlp-error-count

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

Theorem: rlp-error-count-of-rlp-error-fix-x

(defthm rlp-error-count-of-rlp-error-fix-x
  (equal (rlp-error-count (rlp-error-fix x))
         (rlp-error-count x)))

Theorem: rlp-error-count-rlp-error-equiv-congruence-on-x

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

Theorem: rlp-error-count-of-rlp-error-subtree

(defthm rlp-error-count-of-rlp-error-subtree
  (implies t
           (< (+ (rlp-error-count error))
              (rlp-error-count (rlp-error-subtree error))))
  :rule-classes :linear)

Theorem: rlp-error-count-of-rlp-error-subtree->error

(defthm rlp-error-count-of-rlp-error-subtree->error
  (implies (equal (rlp-error-kind x) :subtree)
           (< (rlp-error-count (rlp-error-subtree->error x))
              (rlp-error-count x)))
  :rule-classes :linear)