		Search-engine friendly clone of the ACL2 documentation.

Vl-warningtree

Vl-warningtree-count

Measure for recurring over vl-warningtree structures.

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

Definitions and Theorems

Function: vl-warningtree-count

(defun vl-warningtree-count (x)
 (declare (xargs :guard (vl-warningtree-p x)))
 (let ((__function__ 'vl-warningtree-count))
  (declare (ignorable __function__))
  (common-lisp::case (vl-warningtree-kind x)
   (:null 1)
   (:warning 1)
   (:context (+ 3
                (vl-warningtree-count (vl-warningtree->subtree x))))
   (:pair (+ 3
             (vl-warningtree-count (vl-warningtree->left x))
             (vl-warningtree-count (vl-warningtree->right x)))))))

Theorem: natp-of-vl-warningtree-count

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

Theorem: vl-warningtree-count-of-vl-warningtree-fix-x

(defthm vl-warningtree-count-of-vl-warningtree-fix-x
  (equal (vl-warningtree-count (vl-warningtree-fix x))
         (vl-warningtree-count x)))

Theorem: vl-warningtree-count-vl-warningtree-equiv-congruence-on-x

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

Theorem: vl-warningtree-count-of-vl-warningtree-context

(defthm vl-warningtree-count-of-vl-warningtree-context
 (implies
  t
  (<
   (+ (vl-warningtree-count subtree))
   (vl-warningtree-count (vl-warningtree-context context subtree))))
 :rule-classes :linear)

Theorem: vl-warningtree-count-of-vl-warningtree->subtree

(defthm vl-warningtree-count-of-vl-warningtree->subtree
  (implies (equal (vl-warningtree-kind x) :context)
           (< (vl-warningtree-count (vl-warningtree->subtree x))
              (vl-warningtree-count x)))
  :rule-classes :linear)

Theorem: vl-warningtree-count-of-vl-warningtree-pair

(defthm vl-warningtree-count-of-vl-warningtree-pair
  (implies
       t
       (< (+ (vl-warningtree-count left)
             (vl-warningtree-count right))
          (vl-warningtree-count (vl-warningtree-pair left right))))
  :rule-classes :linear)

Theorem: vl-warningtree-count-of-vl-warningtree->left

(defthm vl-warningtree-count-of-vl-warningtree->left
  (implies (equal (vl-warningtree-kind x) :pair)
           (< (vl-warningtree-count (vl-warningtree->left x))
              (vl-warningtree-count x)))
  :rule-classes :linear)

Theorem: vl-warningtree-count-of-vl-warningtree->right

(defthm vl-warningtree-count-of-vl-warningtree->right
  (implies (equal (vl-warningtree-kind x) :pair)
           (< (vl-warningtree-count (vl-warningtree->right x))
              (vl-warningtree-count x)))
  :rule-classes :linear)