		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstate-fork

Signature
(svstate-fork x) → new-x
Arguments: x — Guard (svstate-p x).
Returns: new-x — Type (svstate-p new-x).

Definitions and Theorems

Function: svstate-fork

(defun svstate-fork (x)
  (declare (xargs :guard (svstate-p x)))
  (let ((__function__ 'svstate-fork))
    (declare (ignorable __function__))
    (b* (((svstate x)))
      (change-svstate x
                      :blkst (svstack-fork x.blkst)
                      :nonblkst (fast-alist-fork x.nonblkst nil)))))

Theorem: svstate-p-of-svstate-fork

(defthm svstate-p-of-svstate-fork
  (b* ((new-x (svstate-fork x)))
    (svstate-p new-x))
  :rule-classes :rewrite)

Theorem: svstate-fork-blkst-len

(defthm svstate-fork-blkst-len
  (b* ((?new-x (svstate-fork x)))
    (equal (len (svstate->blkst new-x))
           (len (svstate->blkst x)))))

Theorem: vars-of-svstate-fork

(defthm vars-of-svstate-fork
  (b* ((?new-x (svstate-fork x)))
    (implies (not (member v (svstate-vars x)))
             (not (member v (svstate-vars new-x))))))

Theorem: svstate-fork-of-svstate-fix-x

(defthm svstate-fork-of-svstate-fix-x
  (equal (svstate-fork (svstate-fix x))
         (svstate-fork x)))

Theorem: svstate-fork-svstate-equiv-congruence-on-x

(defthm svstate-fork-svstate-equiv-congruence-on-x
  (implies (svstate-equiv x x-equiv)
           (equal (svstate-fork x)
                  (svstate-fork x-equiv)))
  :rule-classes :congruence)