		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-maybe-expr-increwrite-aux

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

Definitions and Theorems

Function: vl-maybe-expr-increwrite-aux

(defun vl-maybe-expr-increwrite-aux (x pre post loc)
  (declare (xargs :guard (and (vl-maybe-expr-p x)
                              (vl-stmtlist-p pre)
                              (vl-stmtlist-p post)
                              (vl-location-p loc))))
  (let ((__function__ 'vl-maybe-expr-increwrite-aux))
    (declare (ignorable __function__))
    (if x (vl-expr-increwrite-aux x pre post loc)
      (mv nil (vl-stmtlist-fix pre)
          (vl-stmtlist-fix post)))))

Theorem: vl-maybe-expr-p-of-vl-maybe-expr-increwrite-aux.new-x

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

Theorem: vl-stmtlist-p-of-vl-maybe-expr-increwrite-aux.pre

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

Theorem: vl-stmtlist-p-of-vl-maybe-expr-increwrite-aux.post

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

Theorem: vl-maybe-expr-increwrite-aux-of-vl-maybe-expr-fix-x

(defthm vl-maybe-expr-increwrite-aux-of-vl-maybe-expr-fix-x
  (equal (vl-maybe-expr-increwrite-aux (vl-maybe-expr-fix x)
                                       pre post loc)
         (vl-maybe-expr-increwrite-aux x pre post loc)))

Theorem: vl-maybe-expr-increwrite-aux-vl-maybe-expr-equiv-congruence-on-x

(defthm
   vl-maybe-expr-increwrite-aux-vl-maybe-expr-equiv-congruence-on-x
  (implies
       (vl-maybe-expr-equiv x x-equiv)
       (equal (vl-maybe-expr-increwrite-aux x pre post loc)
              (vl-maybe-expr-increwrite-aux x-equiv pre post loc)))
  :rule-classes :congruence)

Theorem: vl-maybe-expr-increwrite-aux-of-vl-stmtlist-fix-pre

(defthm vl-maybe-expr-increwrite-aux-of-vl-stmtlist-fix-pre
  (equal (vl-maybe-expr-increwrite-aux x (vl-stmtlist-fix pre)
                                       post loc)
         (vl-maybe-expr-increwrite-aux x pre post loc)))

Theorem: vl-maybe-expr-increwrite-aux-vl-stmtlist-equiv-congruence-on-pre

(defthm
   vl-maybe-expr-increwrite-aux-vl-stmtlist-equiv-congruence-on-pre
  (implies
       (vl-stmtlist-equiv pre pre-equiv)
       (equal (vl-maybe-expr-increwrite-aux x pre post loc)
              (vl-maybe-expr-increwrite-aux x pre-equiv post loc)))
  :rule-classes :congruence)

Theorem: vl-maybe-expr-increwrite-aux-of-vl-stmtlist-fix-post

(defthm vl-maybe-expr-increwrite-aux-of-vl-stmtlist-fix-post
  (equal (vl-maybe-expr-increwrite-aux x pre (vl-stmtlist-fix post)
                                       loc)
         (vl-maybe-expr-increwrite-aux x pre post loc)))

Theorem: vl-maybe-expr-increwrite-aux-vl-stmtlist-equiv-congruence-on-post

(defthm
  vl-maybe-expr-increwrite-aux-vl-stmtlist-equiv-congruence-on-post
  (implies
       (vl-stmtlist-equiv post post-equiv)
       (equal (vl-maybe-expr-increwrite-aux x pre post loc)
              (vl-maybe-expr-increwrite-aux x pre post-equiv loc)))
  :rule-classes :congruence)

Theorem: vl-maybe-expr-increwrite-aux-of-vl-location-fix-loc

(defthm vl-maybe-expr-increwrite-aux-of-vl-location-fix-loc
 (equal
     (vl-maybe-expr-increwrite-aux x pre post (vl-location-fix loc))
     (vl-maybe-expr-increwrite-aux x pre post loc)))

Theorem: vl-maybe-expr-increwrite-aux-vl-location-equiv-congruence-on-loc

(defthm
   vl-maybe-expr-increwrite-aux-vl-location-equiv-congruence-on-loc
  (implies
       (vl-location-equiv loc loc-equiv)
       (equal (vl-maybe-expr-increwrite-aux x pre post loc)
              (vl-maybe-expr-increwrite-aux x pre post loc-equiv)))
  :rule-classes :congruence)