(vl-maybe-expr-increwrite-aux x pre post loc) → (mv new-x pre post)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)