(vl-maybe-exprlist-increwrite-aux x pre post loc) → (mv new-x pre post)
Function:
(defun vl-maybe-exprlist-increwrite-aux (x pre post loc) (declare (xargs :guard (and (vl-maybe-exprlist-p x) (vl-stmtlist-p pre) (vl-stmtlist-p post) (vl-location-p loc)))) (let ((__function__ 'vl-maybe-exprlist-increwrite-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil (vl-stmtlist-fix pre) (vl-stmtlist-fix post))) ((mv car pre post) (vl-maybe-expr-increwrite-aux (car x) pre post loc)) ((mv cdr pre post) (vl-maybe-exprlist-increwrite-aux (cdr x) pre post loc))) (mv (cons car cdr) pre post))))
Theorem:
(defthm return-type-of-vl-maybe-exprlist-increwrite-aux.new-x (b* (((mv ?new-x ?pre ?post) (vl-maybe-exprlist-increwrite-aux x pre post loc))) (and (vl-maybe-exprlist-p new-x) (equal (len new-x) (len x)))) :rule-classes :rewrite)
Theorem:
(defthm vl-stmtlist-p-of-vl-maybe-exprlist-increwrite-aux.pre (b* (((mv ?new-x ?pre ?post) (vl-maybe-exprlist-increwrite-aux x pre post loc))) (vl-stmtlist-p pre)) :rule-classes :rewrite)
Theorem:
(defthm vl-stmtlist-p-of-vl-maybe-exprlist-increwrite-aux.post (b* (((mv ?new-x ?pre ?post) (vl-maybe-exprlist-increwrite-aux x pre post loc))) (vl-stmtlist-p post)) :rule-classes :rewrite)
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-of-vl-maybe-exprlist-fix-x (equal (vl-maybe-exprlist-increwrite-aux (vl-maybe-exprlist-fix x) pre post loc) (vl-maybe-exprlist-increwrite-aux x pre post loc)))
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-vl-maybe-exprlist-equiv-congruence-on-x (implies (vl-maybe-exprlist-equiv x x-equiv) (equal (vl-maybe-exprlist-increwrite-aux x pre post loc) (vl-maybe-exprlist-increwrite-aux x-equiv pre post loc))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-of-vl-stmtlist-fix-pre (equal (vl-maybe-exprlist-increwrite-aux x (vl-stmtlist-fix pre) post loc) (vl-maybe-exprlist-increwrite-aux x pre post loc)))
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-vl-stmtlist-equiv-congruence-on-pre (implies (vl-stmtlist-equiv pre pre-equiv) (equal (vl-maybe-exprlist-increwrite-aux x pre post loc) (vl-maybe-exprlist-increwrite-aux x pre-equiv post loc))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-of-vl-stmtlist-fix-post (equal (vl-maybe-exprlist-increwrite-aux x pre (vl-stmtlist-fix post) loc) (vl-maybe-exprlist-increwrite-aux x pre post loc)))
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-vl-stmtlist-equiv-congruence-on-post (implies (vl-stmtlist-equiv post post-equiv) (equal (vl-maybe-exprlist-increwrite-aux x pre post loc) (vl-maybe-exprlist-increwrite-aux x pre post-equiv loc))) :rule-classes :congruence)
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-of-vl-location-fix-loc (equal (vl-maybe-exprlist-increwrite-aux x pre post (vl-location-fix loc)) (vl-maybe-exprlist-increwrite-aux x pre post loc)))
Theorem:
(defthm vl-maybe-exprlist-increwrite-aux-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-maybe-exprlist-increwrite-aux x pre post loc) (vl-maybe-exprlist-increwrite-aux x pre post loc-equiv))) :rule-classes :congruence)