		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-rhs-increwrite

Signature
(vl-rhs-increwrite x loc) → (mv new-x pre post)
Arguments: x — Guard (vl-rhs-p x).; loc — Guard (vl-location-p loc).
Returns: new-x — Type (vl-rhs-p new-x).; pre — Type (vl-stmtlist-p pre).; post — Type (vl-stmtlist-p post).

Definitions and Theorems

Function: vl-rhs-increwrite

(defun vl-rhs-increwrite (x loc)
 (declare (xargs :guard (and (vl-rhs-p x) (vl-location-p loc))))
 (let ((__function__ 'vl-rhs-increwrite))
  (declare (ignorable __function__))
  (b* ((x (vl-rhs-fix x)))
   (vl-rhs-case
    x
    (:vl-rhsexpr (b* (((unless (vl-expr-has-incexprs-p x.guts))
                       (mv x nil nil))
                      ((mv new-guts pre-rev post-rev)
                       (vl-expr-increwrite-aux x.guts nil nil loc)))
                   (mv (change-vl-rhsexpr x :guts new-guts)
                       (rev pre-rev)
                       (rev post-rev))))
    (:vl-rhsnew (b* (((mv new-arrsize pre1 post1)
                      (vl-maybe-expr-increwrite x.arrsize loc))
                     ((mv new-args pre2 post2)
                      (vl-exprlist-increwrite x.args loc)))
                  (mv (change-vl-rhsnew x
                                        :arrsize new-arrsize
                                        :args new-args)
                      (append-without-guard pre1 pre2)
                      (append-without-guard post1 post2))))))))

Theorem: vl-rhs-p-of-vl-rhs-increwrite.new-x

(defthm vl-rhs-p-of-vl-rhs-increwrite.new-x
  (b* (((mv ?new-x ?pre ?post)
        (vl-rhs-increwrite x loc)))
    (vl-rhs-p new-x))
  :rule-classes :rewrite)

Theorem: vl-stmtlist-p-of-vl-rhs-increwrite.pre

(defthm vl-stmtlist-p-of-vl-rhs-increwrite.pre
  (b* (((mv ?new-x ?pre ?post)
        (vl-rhs-increwrite x loc)))
    (vl-stmtlist-p pre))
  :rule-classes :rewrite)

Theorem: vl-stmtlist-p-of-vl-rhs-increwrite.post

(defthm vl-stmtlist-p-of-vl-rhs-increwrite.post
  (b* (((mv ?new-x ?pre ?post)
        (vl-rhs-increwrite x loc)))
    (vl-stmtlist-p post))
  :rule-classes :rewrite)

Theorem: vl-rhs-increwrite-of-vl-rhs-fix-x

(defthm vl-rhs-increwrite-of-vl-rhs-fix-x
  (equal (vl-rhs-increwrite (vl-rhs-fix x) loc)
         (vl-rhs-increwrite x loc)))

Theorem: vl-rhs-increwrite-vl-rhs-equiv-congruence-on-x

(defthm vl-rhs-increwrite-vl-rhs-equiv-congruence-on-x
  (implies (vl-rhs-equiv x x-equiv)
           (equal (vl-rhs-increwrite x loc)
                  (vl-rhs-increwrite x-equiv loc)))
  :rule-classes :congruence)

Theorem: vl-rhs-increwrite-of-vl-location-fix-loc

(defthm vl-rhs-increwrite-of-vl-location-fix-loc
  (equal (vl-rhs-increwrite x (vl-location-fix loc))
         (vl-rhs-increwrite x loc)))

Theorem: vl-rhs-increwrite-vl-location-equiv-congruence-on-loc

(defthm vl-rhs-increwrite-vl-location-equiv-congruence-on-loc
  (implies (vl-location-equiv loc loc-equiv)
           (equal (vl-rhs-increwrite x loc)
                  (vl-rhs-increwrite x loc-equiv)))
  :rule-classes :congruence)