(svstmt-process-writelist x blockingp nb-delayp xcond st) → (mv new-st all-lhs)
Function:
(defun svstmt-process-writelist (x blockingp nb-delayp xcond st) (declare (xargs :guard (and (svstmt-writelist-p x) (svstate-p st)))) (let ((__function__ 'svstmt-process-writelist)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (svstate-fix st) nil)) ((mv st lhs1) (svstmt-process-write (car x) blockingp nb-delayp xcond st)) ((mv st lhs2) (svstmt-process-writelist (cdr x) blockingp nb-delayp xcond st))) (mv st (append-without-guard lhs1 lhs2)))))
Theorem:
(defthm svstate-p-of-svstmt-process-writelist.new-st (b* (((mv ?new-st ?all-lhs) (svstmt-process-writelist x blockingp nb-delayp xcond st))) (svstate-p new-st)) :rule-classes :rewrite)
Theorem:
(defthm lhs-p-of-svstmt-process-writelist.all-lhs (b* (((mv ?new-st ?all-lhs) (svstmt-process-writelist x blockingp nb-delayp xcond st))) (lhs-p all-lhs)) :rule-classes :rewrite)
Theorem:
(defthm svstates-compatible-of-svstmt-process-writelist (b* (((mv ?new-st ?all-lhs) (svstmt-process-writelist x blockingp nb-delayp xcond st))) (implies (consp (svstate->blkst st)) (svstates-compatible new-st st))))
Theorem:
(defthm svarlist-addr-p-of-svstmt-process-writelist (b* (((mv ?new-st ?all-lhs) (svstmt-process-writelist x blockingp nb-delayp xcond st))) (implies (and (svarlist-addr-p (svstmt-writelist-vars x)) (svarlist-addr-p (svstate-vars st))) (svarlist-addr-p (svstate-vars new-st)))))
Theorem:
(defthm svstmt-process-writelist-of-svstmt-writelist-fix-x (equal (svstmt-process-writelist (svstmt-writelist-fix x) blockingp nb-delayp xcond st) (svstmt-process-writelist x blockingp nb-delayp xcond st)))
Theorem:
(defthm svstmt-process-writelist-svstmt-writelist-equiv-congruence-on-x (implies (svstmt-writelist-equiv x x-equiv) (equal (svstmt-process-writelist x blockingp nb-delayp xcond st) (svstmt-process-writelist x-equiv blockingp nb-delayp xcond st))) :rule-classes :congruence)
Theorem:
(defthm svstmt-process-writelist-of-svstate-fix-st (equal (svstmt-process-writelist x blockingp nb-delayp xcond (svstate-fix st)) (svstmt-process-writelist x blockingp nb-delayp xcond st)))
Theorem:
(defthm svstmt-process-writelist-svstate-equiv-congruence-on-st (implies (svstate-equiv st st-equiv) (equal (svstmt-process-writelist x blockingp nb-delayp xcond st) (svstmt-process-writelist x blockingp nb-delayp xcond st-equiv))) :rule-classes :congruence)