		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstmt-process-writelist

Signature
(svstmt-process-writelist x blockingp nb-delayp xcond st) → (mv new-st all-lhs)
Arguments: x — Guard (svstmt-writelist-p x).; st — Guard (svstate-p st).
Returns: new-st — Type (svstate-p new-st).; all-lhs — Concatenation of the static LHSes of all of the writes.
Type (lhs-p all-lhs).

Definitions and Theorems

Function: svstmt-process-writelist

(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: svstate-p-of-svstmt-process-writelist.new-st

(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: lhs-p-of-svstmt-process-writelist.all-lhs

(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: svstates-compatible-of-svstmt-process-writelist

(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: svarlist-addr-p-of-svstmt-process-writelist

(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: svstmt-process-writelist-of-svstmt-writelist-fix-x

(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: svstmt-process-writelist-svstmt-writelist-equiv-congruence-on-x

(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: svstmt-process-writelist-of-svstate-fix-st

(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: svstmt-process-writelist-svstate-equiv-congruence-on-st

(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)