		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-function-specialization-map-increwrite

Signature
(vl-function-specialization-map-increwrite x) → new-x
Arguments: x — Guard (vl-function-specialization-map-p x).
Returns: new-x — Type (vl-function-specialization-map-p new-x).

Definitions and Theorems

Function: vl-function-specialization-map-increwrite

(defun vl-function-specialization-map-increwrite (x)
  (declare (xargs :guard (vl-function-specialization-map-p x)))
  (let ((__function__ 'vl-function-specialization-map-increwrite))
    (declare (ignorable __function__))
    (b* ((x (vl-function-specialization-map-fix x))
         ((when (atom x)) (b* nil nil))
         (fty::val (vl-function-specialization-increwrite (cdar x)))
         (cdr (vl-function-specialization-map-increwrite (cdr x))))
      (cons-with-hint (cons-with-hint (caar x)
                                      fty::val (car x))
                      cdr x))))

Theorem: vl-function-specialization-map-p-of-vl-function-specialization-map-increwrite

(defthm
 vl-function-specialization-map-p-of-vl-function-specialization-map-increwrite
 (b* ((new-x (vl-function-specialization-map-increwrite x)))
   (vl-function-specialization-map-p new-x))
 :rule-classes :rewrite)

Theorem: vl-function-specialization-map-increwrite-of-vl-function-specialization-map-fix-x

(defthm
 vl-function-specialization-map-increwrite-of-vl-function-specialization-map-fix-x
 (equal (vl-function-specialization-map-increwrite
             (vl-function-specialization-map-fix x))
        (vl-function-specialization-map-increwrite x)))

Theorem: vl-function-specialization-map-increwrite-vl-function-specialization-map-equiv-congruence-on-x

(defthm
 vl-function-specialization-map-increwrite-vl-function-specialization-map-equiv-congruence-on-x
 (implies
      (vl-function-specialization-map-equiv x x-equiv)
      (equal (vl-function-specialization-map-increwrite x)
             (vl-function-specialization-map-increwrite x-equiv)))
 :rule-classes :congruence)